Library MetaCoq.PCUIC.PCUICConversion

We develop the equational theory generated by the conversion relation.
  • Congruence lemmas are named ws_cumul_pb_x, for x a term constructor (e.g. Prod, Lambda, App) or term constructing function (mkApps, it_mkLambda..)
  • Inversion lemmas are named ws_cumul_pb_x_inv or ws_cumul_pb_x_y_inv for x, y, term constructors.
For reduction, we use the invert_red_x scheme.
This files derives the injectivity of type constructors for conversion/cumulativity and the discrimination of Sorts, Products and Inductive types. It also shows that conversion is properly congruent for all type and term constructors, as long as we are considering *well-scoped* objects.

Implicit Types (cf : checker_flags) (Σ : global_env_ext).

Set Default Goal Selector "!".

Ltac pcuic := intuition eauto 5 with pcuic ||
  (try solve [repeat red; cbn in *; intuition auto; eauto 5 with pcuic || (try lia || congruence)]).

#[global]
Hint Resolve eq_universe_leq_universe' : pcuic.

Derive Signature for assumption_context.
Derive Signature for clos_refl_trans_1n.

Notation ws_cumul_pb_terms Σ Γ := (All2 (ws_cumul_pb Conv Σ Γ)).

#[global]
Instance ws_cumul_pb_terms_Proper {cf:checker_flags} Σ Γ : CMorphisms.Proper (eq ==> eq ==> arrow)%signatureT (ws_cumul_pb_terms Σ Γ).
Proof. intros x yx' y'f. exact f. Qed.

#[global]
Instance ws_cumul_pb_terms_trans {cf : checker_flags} {Σ : global_env_ext} {wfΣ : wf Σ} Γ : Transitive (ws_cumul_pb_terms Σ Γ).
Proof.
  intros x y z.
  eapply All2_trans; tc.
Qed.

#[global]
Instance ws_cumul_pb_terms_sym {cf} Σ {wfΣ : wf Σ} Γ : Symmetric (ws_cumul_pb_terms Σ Γ).
Proof.
  intros x y.
  eapply All2_symP; tc.
Qed.

#[global] Existing Instance All2_reflexivity.

Section CumulSpecIsCumulAlgo.

  Context {cf:checker_flags} (Σ : global_env_ext).

  Proposition red1_cumulSpec (Γ : context) (M N : term) :
    Σ ;;; Γ |- M N Σ ;;; Γ |- M =s N.
  Proof.
  intro r. induction r using red1_ind_all; try (econstructor; eauto; reflexivity).
  - eapply cumul_Case; try reflexivity.
    × destruct p as [p x]. cbn in ×. try repeat split; cbn; try reflexivity.
      change (fun t uΣ ;;; Γ t s[Conv] u) with (convSpec Σ Γ).
      induction X; econstructor; try reflexivity; try eassumption. exact (p.2).
    × apply All2_reflexivity. eapply Prod_reflexivity; intro x; reflexivity.
  - eapply cumul_Case; try reflexivity.
    × change (fun Γ t uΣ ;;; Γ t s[Conv] u) with (convSpec Σ).
      destruct p as [p x]. cbn in ×. try repeat split; cbn; try reflexivity; eauto.
    × apply All2_reflexivity. eapply Prod_reflexivity; intro x; reflexivity.
  - eapply cumul_Case; try reflexivity.
    × change (fun Γ t uΣ ;;; Γ t s[Conv] u) with (convSpec Σ).
      destruct p as [p x]. cbn in ×. try repeat split; cbn; try reflexivity; eauto.
    × eauto.
    × apply All2_reflexivity. eapply Prod_reflexivity; intro x; reflexivity.
  - eapply cumul_Case; try reflexivity.
    × change (fun Γ t uΣ ;;; Γ t s[Conv] u) with (convSpec Σ).
      destruct p as [p x]. cbn in ×. try repeat split; cbn; try reflexivity; eauto.
    × induction X; econstructor.
      + destruct p0 as [ [ _ hbody ] hhd ]. rewrite hhd. split; eauto. reflexivity.
      + apply All2_reflexivity. eapply Prod_reflexivity; intro x; reflexivity.
      + split; reflexivity.
      + exact IHX.
  - eapply cumul_Evar.
    change (fun t uΣ ;;; Γ t s[Conv] u) with (convSpec Σ Γ).
    induction X; econstructor; eauto; try reflexivity.
    × exact p.2.
  - eapply cumul_Fix. set (mfixAbs := mfix0). unfold mfixAbs at 2. clearbody mfixAbs.
    induction X; econstructor; eauto; try reflexivity.
    × destruct p as [ [ _ hdtype ] e ].
      pose proof (erarg := snd_eq e). pose proof (edbody := snd_eq (fst_eq e)).
      pose proof (edname := fst_eq (fst_eq e)). clear e. destruct erarg, edbody, edname.
      repeat split; eauto ; try reflexivity.
    × apply All2_reflexivity. repeat eapply Prod_reflexivity; intro x; reflexivity.
    × repeat split; reflexivity.
  - eapply cumul_Fix. set (mfixAbs := mfix0). unfold mfixAbs at 2.
    assert (Habs : mfixAbs = mfix0) by reflexivity. clearbody mfixAbs.
    induction X; destruct Habs; econstructor; eauto; try reflexivity.
    × destruct p as [ [ _ hdtype ] e ].
      pose proof (erarg := snd_eq e). pose proof (edbody := snd_eq (fst_eq e)).
      pose proof (edname := fst_eq (fst_eq e)). clear e. destruct erarg, edbody, edname.
      repeat split; eauto ; try reflexivity.
    × apply All2_reflexivity. repeat eapply Prod_reflexivity; intro x; reflexivity.
    × repeat split; reflexivity.
  - eapply cumul_CoFix. set (mfixAbs := mfix0). unfold mfixAbs at 2. clearbody mfixAbs.
    induction X; econstructor; eauto; try reflexivity.
    × destruct p as [ [ _ hdtype ] e ].
      pose proof (erarg := snd_eq e). pose proof (edbody := snd_eq (fst_eq e)).
      pose proof (edname := fst_eq (fst_eq e)). clear e. destruct erarg, edbody, edname.
      repeat split; eauto ; try reflexivity.
    × apply All2_reflexivity. repeat eapply Prod_reflexivity; intro x; reflexivity.
    × repeat split; reflexivity.
  - eapply cumul_CoFix. set (mfixAbs := mfix0). unfold mfixAbs at 2.
    assert (Habs : mfixAbs = mfix0) by reflexivity. clearbody mfixAbs.
    induction X; destruct Habs; econstructor; eauto; try reflexivity.
    × destruct p as [ [ _ hdtype ] e ].
      pose proof (erarg := snd_eq e). pose proof (edbody := snd_eq (fst_eq e)).
      pose proof (edname := fst_eq (fst_eq e)). clear e. destruct erarg, edbody, edname.
      repeat split; eauto ; try reflexivity.
    × apply All2_reflexivity. repeat eapply Prod_reflexivity; intro x; reflexivity.
    × repeat split; reflexivity.
  Defined.

  Proposition convSpec_cumulSpec (Γ : context) (M N : term) :
    Σ ;;; Γ |- M =s N Σ ;;; Γ |- M s N.
  Proof.
    intro Hconv. apply cumul_Sym. apply cumul_Sym. assumption.
  Defined.

  Proposition cumul_mkApps (Γ : context) {pb} M N args args' :
    cumulSpec0 Σ Γ pb M N
    All2 (cumulSpec0 Σ Γ Conv) args args'
    cumulSpec0 Σ Γ pb (mkApps M args) (mkApps N args').
  Proof.
    intros HMN Hargs. revert M N HMN; induction Hargs; intros.
    - eassumption.
    - cbn. eapply IHHargs. eapply cumul_App; eauto.
  Defined.

  Ltac try_with_nil := match goal with H : _ |- _eapply (H _ _ _ [] []); eauto end.

  Proposition eq_term_upto_univ_napp_cumulSpec (Γ : context) {pb} M N args args' :
    compare_term_napp pb Σ Σ #|args| M N
    All2 (cumulSpec0 Σ Γ Conv) args args'
    cumulSpec0 Σ Γ pb (mkApps M args) (mkApps N args').
  Proof.
    induction M in Γ, pb, N , args, args' |- × using term_forall_list_ind ; intros H Hargs; depelim H;
      try (solve [eapply cumul_mkApps; eauto ; econstructor; eauto; try_with_nil]).
    - apply cumul_mkApps; eauto. eapply All2_All_mix_left in X. 2: tea.
      eapply cumul_Evar. eapply All2_impl; try exact X. cbv beta. intuition.
      try_with_nil.
    - eapply (IHM1 _ _ _ (M2 :: args) (u' :: args')); eauto. econstructor; eauto. try_with_nil.
    - eapply cumul_Ind; eauto.
    - eapply cumul_Construct; eauto.
    - apply cumul_mkApps; eauto. unfold tCasePredProp in X. destruct X as [ X [ Xctx Xreturn ]].
      eapply cumul_Case.
      × unfold cumul_predicate, eq_predicate in ×. repeat split.
        + destruct e. eapply All2_All_mix_left in X. 2: tea.
          eapply All2_impl. 1: eassumption. cbn. intuition.
          try_with_nil.
        + intuition.
        + intuition.
        + try_with_nil. intuition.
      × try_with_nil.
      × unfold tCaseBrsProp in X0. eapply All2_All_mix_left in X0. 2: tea.
        eapply All2_impl. 1: eassumption. cbn. intuition.
        try_with_nil.
    - apply cumul_mkApps; eauto. eapply cumul_Fix. unfold tFixProp in ×.
      eapply All2_All_mix_left in X. 2: tea. eapply All2_impl; try exact X. cbv beta. intuition; try_with_nil.
    - apply cumul_mkApps; eauto. eapply cumul_CoFix. unfold tFixProp in ×.
      eapply All2_All_mix_left in X. 2: tea. eapply All2_impl; try exact X. cbv beta. intuition; try_with_nil.
  Defined.

  Proposition eq_term_upto_univ_cumulSpec (Γ : context) {pb} M N :
    compare_term pb Σ Σ M N cumulSpec0 Σ Γ pb M N.
  Proof.
    intros. eapply (eq_term_upto_univ_napp_cumulSpec _ _ _ [] []); eauto.
  Defined.

  Proposition cumulAlgo_cumulSpec {pb} (Γ : context) (M N : term) :
    Σ ;;; Γ M ≤[pb] N Σ ;;; Γ M s[pb] N.
  Proof.
  induction 1.
  - destruct pb; eapply eq_term_upto_univ_cumulSpec; eauto.
  - destruct pb; revgoals.
    × eapply cumul_Trans; eauto. apply convSpec_cumulSpec. apply red1_cumulSpec ; assumption.
    × eapply cumul_Trans; eauto. apply red1_cumulSpec ; assumption.
  - destruct pb; revgoals.
    × eapply cumul_Trans; eauto. apply cumul_Sym. apply red1_cumulSpec ; assumption.
    × eapply cumul_Trans; eauto. apply cumul_Sym. apply red1_cumulSpec ; assumption.
  Defined.

End CumulSpecIsCumulAlgo.

Fixpoint isFixApp t : bool :=
  match t with
  | tApp f uisFixApp f
  | tFix mfix idxtrue
  | _false
  end.

Lemma isFixApp_mkApps :
   t l,
    isFixApp (mkApps t l) = isFixApp t.
Proof.
  intros t l. induction l in t |- ×.
  - cbn. reflexivity.
  - cbn. rewrite IHl. reflexivity.
Qed.

Lemma on_fvs_prod {n na M1 M2} :
  on_free_vars (shiftnP n xpred0) (tProd na M1 M2) =
  on_free_vars (shiftnP n xpred0) M1 &&
  on_free_vars (shiftnP (S n) xpred0) M2.
Proof. cbn. rewrite shiftnP_add. reflexivity. Qed.

Lemma on_fvs_lambda {n na M1 M2} :
  on_free_vars (shiftnP n xpred0) (tLambda na M1 M2) =
  on_free_vars (shiftnP n xpred0) M1 &&
  on_free_vars (shiftnP (S n) xpred0) M2.
Proof. cbn. rewrite shiftnP_add. reflexivity. Qed.

Lemma on_fvs_letin {n na M1 M2 M3} :
  on_free_vars (shiftnP n xpred0) (tLetIn na M1 M2 M3) =
  [&& on_free_vars (shiftnP n xpred0) M1,
  on_free_vars (shiftnP n xpred0) M2 &
  on_free_vars (shiftnP (S n) xpred0) M3].
Proof. cbn. rewrite shiftnP_add. reflexivity. Qed.

Lemma on_free_vars_shiftnP_S (ctx : context) t d :
  on_free_vars (shiftnP #|ctx ,, d| xpred0) t
  on_free_vars (shiftnP (S #|ctx|) xpred0) t.
Proof.
  now len.
Qed.

#[global] Hint Resolve on_free_vars_shiftnP_S : fvs.
#[global] Hint Rewrite @on_fvs_prod @on_fvs_lambda @on_fvs_letin : fvs.
#[global] Hint Rewrite @on_free_vars_ctx_snoc : fvs.
#[global] Hint Resolve closed_red_open_right : fvs.

Ltac fvs := eauto 10 with fvs.
#[global] Hint Resolve eq_universe_leq_universe : core.

Section ConvCongruences.
  Context {cf:checker_flags} {Σ : global_env_ext} {wfΣ : wf Σ}.

  Lemma into_closed_red {Γ t u} :
    red Σ Γ t u
    is_closed_context Γ
    is_open_term Γ t
    Σ ;;; Γ t u.
  Proof using Type.
    now constructor.
  Qed.

  Lemma ws_cumul_pb_Prod_l {Γ na na' M1 M2 N1 pb} :
    eq_binder_annot na na'
    is_open_term (Γ ,, vass na M1) M2
    Σ ;;; Γ M1 = N1
    Σ ;;; Γ (tProd na M1 M2) ≤[pb] (tProd na' N1 M2).
  Proof using wfΣ.
    intros.
    eapply ws_cumul_pb_red in X as (dom & dom' & [rdom rdom' eqdom]); tea.
    eapply ws_cumul_pb_red.
     (tProd na dom M2), (tProd na' dom' M2).
    split; auto.
    - eapply into_closed_red; [eapply red_prod|..]; eauto with fvs.
    - eapply into_closed_red; [eapply red_prod|..]; eauto with fvs.
    - destruct pb; (constructor; [assumption|try apply eqdom|try reflexivity]).
  Qed.

  Lemma ws_cumul_pb_Prod {Γ na na'} {M1 M2 N1 N2} pb :
    eq_binder_annot na na'
    Σ ;;; Γ M1 = N1
    Σ ;;; (Γ ,, vass na M1) M2 ≤[pb] N2
    Σ ;;; Γ (tProd na M1 M2) ≤[pb] (tProd na' N1 N2).
  Proof using wfΣ.
    intros × ? ? ?.
    transitivity (tProd na' N1 M2).
    - eapply ws_cumul_pb_Prod_l; eauto with fvs.
    - eapply (ws_cumul_pb_ws_cumul_ctx (pb':=Conv) (Γ' := Γ ,, vass na' N1)) in X0.
      2:{ constructor. 1:{ eapply ws_cumul_ctx_pb_refl; eauto with fvs. }
          constructor; auto. 1:now symmetry. now symmetry. }
      eapply ws_cumul_pb_red in X0 as (codom & codom' & [rcodom rcodom' eqcodom]).
      eapply ws_cumul_pb_red.
       (tProd na' N1 codom), (tProd na' N1 codom'). split=>//.
      + eapply into_closed_red; [eapply red_prod|..]; fvs.
      + eapply into_closed_red; [eapply red_prod|..]; fvs.
      + destruct pb; (constructor; auto); reflexivity.
  Qed.

  Lemma ws_cumul_pb_Sort_inv {Γ s s'} pb :
    Σ ;;; Γ tSort s ≤[pb] tSort s'
    compare_universe pb Σ s s'.
  Proof using Type.
    intros H; depind H.
    - destruct pb; now inversion c.
    - depelim r. solve_discr.
    - depelim r. solve_discr.
  Qed.

  Lemma ws_cumul_pb_Sort_Prod_inv {Γ s na dom codom} pb :
    Σ ;;; Γ tSort s ≤[pb] tProd na dom codom
    False.
  Proof using Type.
    intros H. depind H.
    - destruct pb; now inversion c.
    - depelim r. solve_discr.
    - depelim r; solve_discr.
      + eapply IHws_cumul_pb. reflexivity.
      + eapply IHws_cumul_pb. reflexivity.
  Qed.

  Lemma ws_cumul_pb_Prod_Sort_inv {Γ s na dom codom} pb :
    Σ ;;; Γ tProd na dom codom ≤[pb] tSort s False.
  Proof using Type.
    intros H; depind H; auto.
    - destruct pb; now inversion c.
    - depelim r.
      + solve_discr.
      + eapply IHws_cumul_pb; reflexivity.
      + eapply IHws_cumul_pb; reflexivity.
    - depelim r. solve_discr.
  Qed.

  Lemma ws_cumul_pb_Sort_l_inv {Γ s T} pb :
    Σ ;;; Γ tSort s ≤[pb] T
     s', Σ ;;; Γ T tSort s' × compare_universe pb Σ s s'.
  Proof using Type.
    intros H. depind H.
    - destruct pb; inversion c; eauto using into_closed_red.
    - depelim r. solve_discr.
    - destruct IHws_cumul_pb as [s' [redv leq]].
       s'. split; auto. eapply into_closed_red; tea.
      eapply red_step with v; eauto with fvs.
  Qed.

  Lemma ws_cumul_pb_Sort_r_inv {Γ s T} pb :
    Σ ;;; Γ T ≤[pb] tSort s
     s', Σ ;;; Γ T tSort s' × compare_universe pb Σ s' s.
  Proof using Type.
    intros H. depind H.
    - destruct pb; inversion c; eauto using into_closed_red.
    - destruct IHws_cumul_pb as [s' [redv leq]].
       s'. split; auto. eapply into_closed_red; tea.
      eapply red_step with v; eauto with fvs.
    - depelim r. solve_discr.
  Qed.



  Lemma closed_red_clos {Γ t u} :
    closed_red Σ Γ t u
    clos_refl_trans (closed_red1 Σ Γ) t u.
  Proof using wfΣ.
    intros [clΓ clt r].
    assert (clu := red_on_free_vars r clt byfvs).
    unshelve eapply (red_ws_red _ (exist Γ clΓ) (exist t byfvs) (exist u _)) in r; cbn; eauto with fvs.
    depind r. all:try solve [econstructor; split; eauto with fvs].
    destruct y as [y hy]; econstructor 3; [eapply IHr1|eapply IHr2]; reflexivity.
  Qed.

  Lemma on_free_vars_subst {Γ Γ' : context} {s b} :
    forallb (on_free_vars (shiftnP #|Γ| xpred0)) s
    on_free_vars (shiftnP (#|Γ| + #|s| + #|Γ'|) xpred0) b
    on_free_vars (shiftnP (#|Γ'| + #|Γ|) xpred0) (subst s #|Γ'| b).
  Proof using Type.
    intros.
    eapply on_free_vars_impl.
    2:eapply on_free_vars_subst_gen; tea.
    intros i.
    rewrite /substP /shiftnP !orb_false_r.
    repeat nat_compare_specs ⇒ //. cbn.
    repeat nat_compare_specs ⇒ //.
  Qed.

  Lemma is_closed_subst_context Γ Δ s Γ' :
    is_closed_context (Γ ,,, Δ ,,, Γ')
    forallb (on_free_vars (shiftnP #|Γ| xpred0)) s
    #|s| = #|Δ|
    is_closed_context (Γ,,, subst_context s 0 Γ').
  Proof using Type.
    rewrite !on_free_vars_ctx_app.
    move/andP ⇒ [] /andP[] → /= onΔ onΓ' ons Hs.
    apply on_free_vars_ctx_subst_context0.
    × rewrite shiftnP_add Hs. now len in onΓ'.
    × eapply All_forallb. solve_all; eauto with fvs.
  Qed.

  Lemma is_open_term_subst_gen {Γ Δ Γ' s s' b} :
    is_closed_context (Γ ,,, Δ ,,, Γ')
    forallb (on_free_vars (shiftnP #|Γ| xpred0)) s
    forallb (on_free_vars (shiftnP #|Γ| xpred0)) s'
    #|s| = #|Δ| #|s| = #|s'|
    is_open_term (Γ,,, Δ,,, Γ') b
    is_open_term (Γ,,, subst_context s 0 Γ') (subst s' #|Γ'| b).
  Proof using Type.
    len; intros. apply on_free_vars_subst. 1:solve_all; eauto with fvs.
    len in H2. rewrite -H3 H2.
    red. rewrite -H4; lia_f_equal.
  Qed.

  Lemma is_open_term_subst {Γ Δ Γ' s b} :
    is_closed_context (Γ ,,, Δ ,,, Γ')
    forallb (on_free_vars (shiftnP #|Γ| xpred0)) s
    #|s| = #|Δ|
    is_open_term (Γ,,, Δ,,, Γ') b
    is_open_term (Γ,,, subst_context s 0 Γ') (subst s #|Γ'| b).
  Proof using Type.
    intros. now eapply is_open_term_subst_gen; tea.
  Qed.

  Lemma closed_red_red_subst {Γ Δ Γ' s s' b} :
    is_closed_context (Γ ,,, Δ ,,, Γ')
    All2 (closed_red Σ Γ) s s'
    untyped_subslet Γ s Δ
    is_open_term (Γ ,,, Δ ,,, Γ') b
    Σ ;;; Γ ,,, subst_context s 0 Γ' subst s #|Γ'| b subst s' #|Γ'| b.
  Proof using wfΣ.
    intros.
    split; eauto with fvs.
    - eapply is_closed_subst_context; tea. 1:solve_all; eauto with fvs.
      now rewrite (untyped_subslet_length X0).
    - eapply is_open_term_subst; tea.
      1:solve_all; eauto with fvs.
      now rewrite (untyped_subslet_length X0).
    - eapply red_red; tea; eauto with fvs.
      × solve_all. exact X.
      × solve_all. len.
        rewrite Nat.add_assoc -shiftnP_add addnP_shiftnP; eauto with fvs.
  Qed.

  Lemma closed_red_red_subst0 {Γ Δ s s' b} :
    is_closed_context (Γ ,,, Δ)
    All2 (closed_red Σ Γ) s s'
    untyped_subslet Γ s Δ
    is_open_term (Γ ,,, Δ) b
    Σ ;;; Γ subst0 s b subst0 s' b.
  Proof using wfΣ.
    intros. eapply (closed_red_red_subst (Γ' := [])); tea.
  Qed.

  Hint Resolve closed_red_red : pcuic.


  Hint Resolve untyped_subslet_length : pcuic.


  Lemma closed_red_untyped_substitution {Γ Δ Γ' s M N} :
    untyped_subslet Γ s Δ
    forallb (on_free_vars (shiftnP #|Γ| xpred0)) s
    Σ ;;; Γ ,,, Δ ,,, Γ' M N
    Σ ;;; Γ ,,, subst_context s 0 Γ' subst s #|Γ'| M subst s #|Γ'| N.
  Proof using wfΣ.
    intros Hs H. split.
    - eapply is_closed_subst_context; eauto with fvs pcuic.
    - eapply is_open_term_subst; tea; eauto with fvs pcuic.
    - eapply substitution_untyped_red; tea; eauto with fvs.
  Qed.

  Lemma closed_red_untyped_substitution0 {Γ Δ s M N} :
    untyped_subslet Γ s Δ
    forallb (on_free_vars (shiftnP #|Γ| xpred0)) s
    Σ ;;; Γ ,,, Δ M N
    Σ ;;; Γ subst s 0 M subst s 0 N.
  Proof using wfΣ.
    intros Hs H. now apply (closed_red_untyped_substitution (Γ' := [])).
  Qed.

  Lemma untyped_subslet_def_tip {Γ na d ty} : untyped_subslet Γ [d] [vdef na d ty].
  Proof using Type.
    rewrite -{1}(subst_empty 0 d). constructor. constructor.
  Qed.
  Hint Resolve untyped_subslet_def_tip : pcuic.

  Lemma invert_red_letin {Γ C na d ty b} :
    Σ ;;; Γ (tLetIn na d ty b) C
    ( d' ty' b',
     C = tLetIn na d' ty' b', Σ ;;; Γ d d', Σ ;;; Γ ty ty' &
      Σ ;;; (Γ ,, vdef na d ty) b b']) +
    (Σ ;;; Γ (subst10 d b) C)%type.
  Proof using wfΣ.
    generalize_eq x (tLetIn na d ty b).
    movee [clΓ clt] red.
    assert (clC : is_open_term Γ C) by eauto with fvs.
    revert na d ty b e.
    eapply clos_rt_rt1n_iff in red.
    induction red; simplify_dep_elim.
    + autorewrite with fvs in clC; move/and3P: clC ⇒ [] ond onty onb.
      left; do 3 eexists. split; eauto with pcuic fvs.
    + assert (is_open_term Γ y) by eauto with fvs. intuition auto.
      autorewrite with fvs in clt; move/and3P: clt ⇒ [] ond onty onb.
      depelim r; try specialize (X0 _ _ _ _ eq_refl) as
        [(? & ? & ? & [? ? ? ?])|?].
      - right. split; try apply clos_rt_rt1n_iff; eauto.
      - solve_discr.
      - left. do 3 eexists; split; eauto with pcuic.
        × transitivity r; eauto with pcuic.
        × eapply red_red_ctx_inv'; eauto.
          simpl. constructor.
          1:{ apply closed_red_ctx_refl ⇒ //. }
          constructor. all:constructor; eauto with fvs.
      - right; auto. transitivity (b {0 := r}); auto.
        eapply (closed_red_red_subst (Δ := [vass na ty]) (Γ' := [])); eauto with fvs.
        × constructor; [|constructor]. eapply into_closed_red; eauto with fvs.
        × constructor. constructor.
      - left. do 3 eexists. repeat split; eauto with pcuic.
        × transitivity r; pcuic.
        × eauto with fvs.
        × eapply red_red_ctx_inv' in c1; [exact c1|].
          simpl. constructor; [now apply closed_red_ctx_refl|].
          constructor; eauto with fvs pcuic.
      - right; auto.
      - left. do 3 eexists. split; tea.
        now transitivity r; eauto with pcuic fvs.
      - right; auto.
        transitivity (r {0 := d}); auto.
        eapply (closed_red_untyped_substitution (Δ := [vdef na d ty]) (Γ' := [])); cbn; eauto with pcuic fvs.
  Qed.

  Lemma invert_red_prod {Γ na dom codom T} :
    Σ ;;; Γ tProd na dom codom T
     dom' codom',
       T = tProd na dom' codom', Σ ;;; Γ dom dom' &
         Σ ;;; Γ ,, vass na dom codom codom'].
  Proof using wfΣ.
    generalize_eq x (tProd na dom codom).
    movee [clΓ clt] red.
    revert na dom codom e.
    eapply clos_rt_rt1n_iff in red.
    induction red; simplify_dep_elim.
    - move: clt.
      rewrite on_fvs_prod ⇒ /andP[] ondom oncodom.
       dom, codom; repeat split; eauto with fvs.
    - move: clt; rewrite on_fvs_prod ⇒ /andP [] ondom oncodom.
      forward IHred. { eapply red1_on_free_vars; tea; eauto with fvs. }
      depelim r; solve_discr.
      × specialize (IHred _ _ _ eq_refl).
        destruct IHred as [dom' [codom' [-> [redl redr]]]].
        eexists _, _; split ⇒ //.
        { transitivity N1; split; eauto with fvs. }
        { eapply red_red_ctx_inv'; tea. constructor; eauto with fvs.
          { now eapply closed_red_ctx_refl. }
          constructor; split; eauto with fvs. }
      × specialize (IHred _ _ _ eq_refl) as [dom' [codom' [-> [redl redr]]]].
        eexists _, _; split ⇒ //.
        transitivity N2; split; eauto with fvs.
  Qed.


  Hint Resolve ws_cumul_pb_compare : pcuic.

  Lemma ws_cumul_pb_Prod_l_inv {pb Γ na dom codom T} :
    Σ ;;; Γ tProd na dom codom ≤[pb] T
     na' dom' codom',
     Σ ;;; Γ T (tProd na' dom' codom'),
      (eq_binder_annot na na'), Σ ;;; Γ dom = dom' &
      Σ ;;; Γ ,, vass na dom codom ≤[pb] codom'].
  Proof using wfΣ.
    intros H.
    eapply ws_cumul_pb_red in H as (v & v' & [tv tv' eqp]).
    destruct (invert_red_prod tv) as (dom' & codom' & [-> reddom redcod]).
    destruct pb.
    - depelim eqp.
      generalize (closed_red_open_right tv').
      rewrite on_fvs_prod ⇒ /andP[] // ona' onb'.
       na', a', b'; split ⇒ //.
      × transitivity dom'; pcuic.
        eapply ws_cumul_pb_compare; eauto with fvs.
      × transitivity codom'; pcuic.
        eapply ws_cumul_pb_compare; eauto with fvs.
    - depelim eqp.
      generalize (closed_red_open_right tv').
      rewrite on_fvs_prod ⇒ /andP[] // ona' onb'.
       na', a', b'; split ⇒ //.
      × transitivity dom'; pcuic.
        eapply ws_cumul_pb_compare; eauto with fvs.
      × transitivity codom'; pcuic.
        eapply ws_cumul_pb_compare; eauto with fvs.
  Qed.

  Lemma ws_cumul_pb_Prod_r_inv {pb Γ na dom codom T} :
    Σ ;;; Γ T ≤[pb] tProd na dom codom
     na' dom' codom',
     Σ ;;; Γ T (tProd na' dom' codom'),
      eq_binder_annot na na',
      Σ ;;; Γ dom' = dom &
      Σ ;;; Γ ,, vass na dom codom' ≤[pb] codom].
  Proof using wfΣ.
    intros H.
    eapply ws_cumul_pb_red in H as (v & v' & [tv tv' eqp]).
    destruct (invert_red_prod tv') as (dom' & codom' & [-> reddom redcod]).
    destruct pb.
    - depelim eqp.
      generalize (closed_red_open_right tv).
      rewrite on_fvs_prod ⇒ /andP[] // ona' onb'.
       na0, a, b; split ⇒ //.
      × transitivity dom'; pcuic.
        eapply ws_cumul_pb_compare; eauto with fvs.
      × transitivity codom'; pcuic.
        eapply ws_cumul_pb_compare; eauto with fvs.
    - depelim eqp.
      generalize (closed_red_open_right tv).
      rewrite on_fvs_prod ⇒ /andP[] // ona' onb'.
       na0, a, b; split ⇒ //.
      × transitivity dom'; pcuic.
        eapply ws_cumul_pb_compare; eauto with fvs.
      × transitivity codom'; pcuic.
        eapply ws_cumul_pb_compare; eauto with fvs.
  Qed.

  Ltac splits := repeat split.

  Lemma ws_cumul_pb_Prod_Prod_inv {pb Γ na na' dom dom' codom codom'} :
    Σ ;;; Γ tProd na dom codom ≤[pb] tProd na' dom' codom'
     eq_binder_annot na na', Σ ;;; Γ dom = dom' & Σ ;;; Γ ,, vass na' dom' codom ≤[pb] codom'].
  Proof using wfΣ.
    intros H.
    eapply ws_cumul_pb_red in H as (v & v' & [tv tv' eqp]).
    destruct (invert_red_prod tv) as (dom0 & codom0 & [-> reddom0 redcod0]).
    destruct (invert_red_prod tv') as (dom0' & codom0' & [-> reddom0' redcod0']).
    destruct pb.
    - depelim eqp.
      assert (Σ ;;; Γ dom = dom').
      { transitivity dom0; pcuic.
        transitivity dom0'; pcuic.
        eapply ws_cumul_pb_compare; eauto with fvs. }
      split ⇒ //.
      transitivity codom0'; pcuic.
      transitivity codom0; pcuic.
      { eapply PCUICContextConversion.ws_cumul_pb_ws_cumul_ctx_inv; pcuic.
        constructor; [apply ws_cumul_ctx_pb_refl|]; eauto with fvs.
        constructor; auto. exact X. }
      constructor; eauto with fvs.
      cbn. eauto with fvs.
    - depelim eqp.
      assert (Σ ;;; Γ dom = dom').
      { transitivity dom0; pcuic.
        transitivity dom0'; pcuic.
        eapply ws_cumul_pb_compare; eauto with fvs. }
      split ⇒ //.
      transitivity codom0'; pcuic.
      transitivity codom0; pcuic.
      { eapply PCUICContextConversion.ws_cumul_pb_ws_cumul_ctx_inv; pcuic.
        constructor; [apply ws_cumul_ctx_pb_refl|]; eauto with fvs.
        constructor; auto. exact X. }
      constructor. 2:cbn. all:eauto with fvs.
  Qed.

End ConvCongruences.

Notation red_terms Σ Γ := (All2 (closed_red Σ Γ)).

Lemma red_terms_ws_cumul_pb_terms {cf} {Σ} {wfΣ : wf Σ} {Γ u u'} :
  red_terms Σ Γ u u' ws_cumul_pb_terms Σ Γ u u'.
Proof.
  moveHu; eapply All2_impl; eauto. intros.
  now eapply red_ws_cumul_pb.
Qed.

Lemma eq_terms_ws_cumul_pb_terms {cf} {Σ} {wfΣ : wf Σ} Γ u u' :
  is_closed_context Γ
  forallb (is_open_term Γ) u
  forallb (is_open_term Γ) u'
  All2 (eq_term Σ Σ) u u' ws_cumul_pb_terms Σ Γ u u'.
Proof.
  moveonΓ onu onu' Hu; solve_all.
  intros. econstructor; eauto.
Qed.

Lemma closed_red_letin {Σ Γ na d0 d1 t0 t1 b0 b1} :
  Σ ;;; Γ d0 d1
  Σ ;;; Γ t0 t1
  Σ ;;; Γ ,, vdef na d1 t1 b0 b1
  Σ ;;; Γ tLetIn na d0 t0 b0 tLetIn na d1 t1 b1.
Proof.
  intros.
  eapply into_closed_red; fvs.
  eapply (red_letin _ _ _ _ _ _ _ X X0 X1).
Qed.

Lemma on_free_vars_ctx_snoc_ass_inv P Γ na t :
  on_free_vars_ctx P (Γ ,, vass na t)
  on_free_vars_ctx P Γ on_free_vars (shiftnP #|Γ| P) t.
Proof.
  rewrite on_free_vars_ctx_snoc ⇒ /andP[]; auto.
Qed.

Lemma on_free_vars_ctx_snoc_def_inv P Γ na b t :
  on_free_vars_ctx P (Γ ,, vdef na b t)
  [/\ on_free_vars_ctx P Γ,
      on_free_vars (shiftnP #|Γ| P) b &
      on_free_vars (shiftnP #|Γ| P) t].
Proof.
  rewrite on_free_vars_ctx_snoc ⇒ /andP[] onΓ /andP[] /=; split; auto.
Qed.

Lemma closed_red_letin_body {Σ Γ na d t b0 b1} :
  Σ ;;; Γ ,, vdef na d t b0 b1
  Σ ;;; Γ tLetIn na d t b0 tLetIn na d t b1.
Proof.
  intros.
  eapply closed_red_letin ⇒ //;
  apply clrel_ctx, on_free_vars_ctx_snoc_def_inv in X as []; now apply closed_red_refl.
Qed.

Lemma closed_red_prod {Σ Γ na A B A' B'} :
  Σ ;;; Γ A A'
  Σ ;;; Γ ,, vass na A B B'
  Σ ;;; Γ tProd na A B tProd na A' B'.
Proof.
  intros h1 h2.
  eapply into_closed_red; fvs.
  eapply red_prod; auto.
  × apply h1.
  × apply h2.
Qed.

Lemma closed_red_prod_codom {Σ Γ na A B B'} :
  Σ ;;; Γ ,, vass na A B B'
  Σ ;;; Γ tProd na A B tProd na A B'.
Proof.
  intros; apply closed_red_prod ⇒ //.
  apply clrel_ctx, on_free_vars_ctx_snoc_ass_inv in X as []. now apply closed_red_refl.
Qed.

Section Inversions.
  Context {cf : checker_flags}.
  Context {Σ : global_env_ext}.
  Context {wfΣ : wf Σ}.

  Definition Is_conv_to_Arity Σ Γ T :=
     T', Σ ;;; Γ T T' isArity T'.

  Lemma arity_red_to_prod_or_sort :
     Γ T,
      is_closed_context Γ
      is_open_term Γ T
      isArity T
      ( na A B, Σ ;;; Γ T (tProd na A B) )
      ( u, Σ ;;; Γ T (tSort u) ).
  Proof using wfΣ.
    intros Γ T.
    induction T in Γ |- ×. all: try contradiction.
    - right. eexists. constructor. pcuic.
    - left. eexists _,_,_. constructor. pcuic.
    - intros clΓ clt a. simpl in a. eapply IHT3 in a as [[na' [A [B [r]]]] | [u [r]]].
      + left. eexists _,_,_. constructor.
        etransitivity.
        × eapply into_closed_red; tas.
          eapply red1_red. eapply red_zeta.
        × eapply (closed_red_untyped_substitution0 (s:=[T1])) in r.
          -- simpl in r. eassumption.
          -- instantiate (1 := [],, vdef na T1 T2).
             replace (untyped_subslet Γ [T1] ([],, vdef na T1 T2))
              with (untyped_subslet Γ [subst0 [] T1] ([],, vdef na T1 T2))
              by (now rewrite subst_empty).
             eapply untyped_cons_let_def.
             constructor.
          -- inv_on_free_vars. cbn. now rewrite p.
      + right. eexists. constructor.
        etransitivity.
        × eapply into_closed_red; tas. eapply red1_red, red_zeta.
        × eapply (closed_red_untyped_substitution0 (s := [T1])) in r.
          -- simpl in r. eassumption.
          -- replace (untyped_subslet Γ [T1] ([],, vdef na T1 T2))
              with (untyped_subslet Γ [subst0 [] T1] ([],, vdef na T1 T2))
              by (now rewrite subst_empty).
            eapply untyped_cons_let_def.
            constructor.
          -- cbn. inv_on_free_vars. now rewrite p.
      + inv_on_free_vars. apply on_free_vars_ctx_snoc_def ⇒ //.
      + inv_on_free_vars. cbn. now setoid_rewrite shiftnP_add in p1.
  Qed.

  Lemma Is_conv_to_Arity_inv :
     Γ T,
      Is_conv_to_Arity Σ Γ T
      ( na A B, Σ ;;; Γ T (tProd na A B) )
      ( u, Σ ;;; Γ T (tSort u) ).
  Proof using wfΣ.
    intros Γ T [T' [r a]].
    induction T'.
    all: try contradiction.
    - right. eexists. eassumption.
    - left. eexists _, _, _. eassumption.
    - destruct r as [r1].
      eapply arity_red_to_prod_or_sort in a as [[na' [A [B [r2]]]] | [u [r2]]].
      + left. eexists _,_,_. constructor.
        etransitivity; tea.
      + right. eexists. constructor.
        etransitivity; tea.
      + fvs.
      + now eapply closed_red_open_right in r1.
  Qed.

  Lemma invert_red_sort Γ u v :
    Σ ;;; Γ (tSort u) v v = tSort u.
  Proof using wfΣ.
    intros [clΓ clu H]. generalize_eq x (tSort u).
    induction H; simplify ×.
    - depind r. solve_discr.
    - reflexivity.
    - rewrite IHclos_refl_trans2; eauto with fvs.
  Qed.

  Lemma eq_term_upto_univ_conv_arity_l :
     Re Rle Γ u v,
      isArity u
      is_closed_context Γ
      is_open_term Γ u
      is_open_term Γ v
      eq_term_upto_univ Σ Re Rle u v
      Is_conv_to_Arity Σ Γ v.
  Proof using Type.
    intros Re Rle Γ u v a clΓ clu clv e.
    induction u in Γ, clΓ, clv, clu, a, v, Rle, e |- ×. all: try contradiction.
    all: dependent destruction e.
    - eexists. split.
      + constructor. eapply closed_red_refl ⇒ //.
      + reflexivity.
    - repeat inv_on_free_vars.
      eapply (IHu2 _ (Γ ,, vass na' a')) in e3; tea.
      × destruct e3 as [b'' [[r] ab]].
         (tProd na' a' b''). split.
        + constructor. now eapply closed_red_prod_codom.
        + simpl. assumption.
      × rewrite on_free_vars_ctx_snoc /on_free_vars_decl /test_decl /= a0 clΓ //.
      × len. now setoid_rewrite shiftnP_add in b0.
      × len. now setoid_rewrite shiftnP_add in b.
    - repeat inv_on_free_vars.
      eapply (IHu3 _ (Γ ,, vdef na' t' ty')) in e4; tea.
      × destruct e4 as [u'' [[r] au]].
         (tLetIn na' t' ty' u''). split.
        + constructor. now eapply closed_red_letin_body.
        + simpl. assumption.
      × now rewrite on_free_vars_ctx_snoc clΓ /on_free_vars_decl /test_decl /= p p0.
      × len. now setoid_rewrite shiftnP_add in p4.
      × len. now setoid_rewrite shiftnP_add in p1.
  Qed.

  Lemma eq_term_upto_univ_conv_arity_r :
     Re Rle Γ u v,
    isArity u
    is_closed_context Γ
    is_open_term Γ u
    is_open_term Γ v
    eq_term_upto_univ Σ Re Rle v u
    Is_conv_to_Arity Σ Γ v.
  Proof using Type.
    intros Re Rle Γ u v a clΓ clu clv e.
    induction u in Γ, clΓ, clv, clu, a, v, Rle, e |- ×. all: try contradiction.
    all: dependent destruction e.
    - eexists. split.
      + constructor. eapply closed_red_refl ⇒ //.
      + reflexivity.
    - repeat inv_on_free_vars.
      simpl in a.
      eapply (IHu2 _ (Γ ,, vass na0 a0)) in e3; tea.
      × destruct e3 as [b'' [[r] ab]].
         (tProd na0 a0 b''). split.
        + constructor. now eapply closed_red_prod_codom.
        + simpl. assumption.
      × rewrite on_free_vars_ctx_snoc /on_free_vars_decl /test_decl /= a1 clΓ //.
      × len. now setoid_rewrite shiftnP_add in b1.
      × len. now setoid_rewrite shiftnP_add in b0.
    - repeat inv_on_free_vars.
      eapply (IHu3 _ (Γ ,, vdef na0 t ty)) in e4; tea.
      × destruct e4 as [u'' [[r] au]].
         (tLetIn na0 t ty u''). split.
        + constructor. now eapply closed_red_letin_body.
        + simpl. assumption.
      × now rewrite on_free_vars_ctx_snoc clΓ /on_free_vars_decl /test_decl /= p p0.
      × len. now setoid_rewrite shiftnP_add in p4.
      × len. now setoid_rewrite shiftnP_add in p1.
  Qed.

  Lemma isArity_subst :
     u v k,
      isArity u
      isArity (u { k := v }).
  Proof using Type.
    intros u v k h.
    induction u in v, k, h |- ×. all: try contradiction.
    - simpl. constructor.
    - simpl in ×. eapply IHu2. assumption.
    - simpl in ×. eapply IHu3. assumption.
  Qed.

  Lemma isArity_red1 :
     Γ u v,
      red1 Σ Γ u v
      isArity u
      isArity v.
  Proof using Type.
    intros Γ u v h a.
    induction u in Γ, v, h, a |- ×. all: try contradiction.
    - dependent destruction h.
      apply (f_equal nApp) in H as eq. simpl in eq.
      rewrite nApp_mkApps in eq. simpl in eq.
      destruct args. 2: discriminate.
      simpl in H. discriminate.
    - dependent destruction h.
      + apply (f_equal nApp) in H as eq. simpl in eq.
        rewrite nApp_mkApps in eq. simpl in eq.
        destruct args. 2: discriminate.
        simpl in H. discriminate.
      + assumption.
      + simpl in ×. eapply IHu2. all: eassumption.
    - dependent destruction h.
      + simpl in ×. apply isArity_subst. assumption.
      + apply (f_equal nApp) in H as eq. simpl in eq.
        rewrite nApp_mkApps in eq. simpl in eq.
        destruct args. 2: discriminate.
        simpl in H. discriminate.
      + assumption.
      + assumption.
      + simpl in ×. eapply IHu3. all: eassumption.
  Qed.

  Lemma invert_cumul_arity_r :
     (Γ : context) (C : term) T,
      isArity T
      Σ;;; Γ C T
      Is_conv_to_Arity Σ Γ C.
  Proof using Type.
    intros Γ C T a h.
    induction h.
    - eapply eq_term_upto_univ_conv_arity_r. all: eassumption.
    - forward IHh by assumption. destruct IHh as [v' [[r'] a']].
       v'. split.
      + constructor. transitivity v ⇒ //.
        eapply into_closed_red ⇒ //.
        now eapply red1_red.
      + assumption.
    - eapply IHh. eapply isArity_red1. all: eassumption.
  Qed.

  Lemma invert_cumul_arity_l :
     (Γ : context) (C : term) T,
      isArity C
      Σ;;; Γ C T
      Is_conv_to_Arity Σ Γ T.
  Proof using Type.
    intros Γ C T a h.
    induction h.
    - eapply eq_term_upto_univ_conv_arity_l. all: eassumption.
    - eapply IHh. eapply isArity_red1. all: eassumption.
    - forward IHh by assumption. destruct IHh as [v' [[r'] a']].
       v'. split.
      + constructor. transitivity v ⇒ //.
        eapply into_closed_red ⇒ //.
        now eapply red1_red.
      + assumption.
  Qed.

  Hint Constructors All_decls : core.

  Lemma ws_cumul_pb_red_r_inv {Γ T} U {U'} {pb} :
    Σ ;;; Γ T ≤[pb] U
    red Σ Γ U U'
    Σ ;;; Γ T ≤[pb] U'.
  Proof using wfΣ.
    intros × cumtu red.
    transitivity U; tea. eapply red_ws_cumul_pb.
    constructor; eauto with fvs.
  Qed.

  Lemma ws_cumul_pb_red_l_inv {Γ} T {T' U} {pb} :
    Σ ;;; Γ T ≤[pb] U
    red Σ Γ T T'
    Σ ;;; Γ T' ≤[pb] U.
  Proof using wfΣ.
    intros × cumtu red.
    transitivity T ⇒ //. eapply red_ws_cumul_pb_inv.
    constructor; eauto with fvs.
  Qed.

  Lemma ws_cumul_pb_LetIn_l_inv {Γ C na d ty b} {pb} :
    Σ ;;; Γ tLetIn na d ty b ≤[pb] C
    Σ ;;; Γ subst10 d b ≤[pb] C.
  Proof using wfΣ.
    intros Hlet.
    eapply ws_cumul_pb_red_l_inv; eauto.
    eapply red1_red; constructor.
  Qed.

  Lemma ws_cumul_pb_LetIn_r_inv {Γ C na d ty b} {pb} :
    Σ ;;; Γ C ≤[pb] tLetIn na d ty b
    Σ ;;; Γ C ≤[pb] subst10 d b.
  Proof using wfΣ.
    intros Hlet.
    eapply ws_cumul_pb_red_r_inv; eauto.
    eapply red1_red; constructor.
  Qed.

  Lemma app_mkApps :
     u v t l,
      isApp t = false
      tApp u v = mkApps t l
       l',
        (l = l' ++ [v]) ×
        u = mkApps t l'.
  Proof using Type.
    intros u v t l h e.
    induction l in u, v, t, e, h |- × using list_rect_rev.
    - cbn in e. subst. cbn in h. discriminate.
    - rewrite mkApps_app in e. cbn in e.
       l. inversion e. subst. auto.
  Qed.

  Lemma invert_red_mkApps_tInd {Γ : context} {ind u} (args : list term) c :
    Σ ;;; Γ mkApps (tInd ind u) args c
     args' : list term,
     c = mkApps (tInd ind u) args', is_closed_context Γ & All2 (closed_red Σ Γ) args args'].
  Proof using wfΣ.
    move⇒ [clΓ].
    rewrite PCUICOnFreeVars.on_free_vars_mkApps ⇒ /= hargs r.
    destruct (red_mkApps_tInd (Γ := exist Γ clΓ) hargs r) as [args' [eq red]].
     args'; split ⇒ //.
    solve_all; split; eauto with fvs.
  Qed.

  Notation invert_red_ind := red_mkApps_tInd.

  Lemma compare_term_mkApps_l_inv {pb} {u : term} {l : list term} {t : term} :
    compare_term pb Σ Σ (mkApps u l) t
     (u' : term) (l' : list term),
       eq_term_upto_univ_napp Σ (eq_universe Σ) (compare_universe pb Σ) #|l| u u',
        All2 (eq_term Σ Σ) l l' & t = mkApps u' l'].
  Proof using wfΣ.
    destruct pb ⇒ /= ⇒ /eq_term_upto_univ_mkApps_l_inv; firstorder.
  Qed.

  Lemma compare_term_mkApps_r_inv {pb} {u : term} {l : list term} {t : term} :
    compare_term pb Σ Σ t (mkApps u l)
     (u' : term) (l' : list term),
       eq_term_upto_univ_napp Σ (eq_universe Σ) (compare_universe pb Σ) #|l| u' u,
        All2 (eq_term Σ Σ) l' l & t = mkApps u' l'].
  Proof using wfΣ.
    destruct pb ⇒ /= ⇒ /eq_term_upto_univ_mkApps_r_inv; firstorder.
  Qed.

  Lemma ws_cumul_pb_Ind_l_inv {pb Γ ind ui l T} :
    Σ ;;; Γ mkApps (tInd ind ui) l ≤[pb] T
     ui' l',
       Σ ;;; Γ T (mkApps (tInd ind ui') l'),
      R_global_instance Σ (eq_universe Σ) (compare_universe pb Σ) (IndRef ind) #|l| ui ui' &
      All2 (fun a a'Σ ;;; Γ a = a') l l'].
  Proof using wfΣ.
    move/ws_cumul_pb_red⇒ [v [v' [redv redv' leqvv']]].
    eapply invert_red_mkApps_tInd in redv as [l' [? ? ha]]; auto. subst.
    eapply compare_term_mkApps_l_inv in leqvv' as [u [l'' [e ? ?]]].
    subst. depelim e.
    eexists _,_. split ; eauto.
    - now rewrite (All2_length ha).
    - eapply All2_trans.
      × intros x y z h1 h2. etransitivity; tea.
      × eapply All2_impl ; eauto with pcuic.
      × assert (forallb (is_open_term Γ) l'). { eapply All_forallb, All2_All_right; tea; eauto with fvs. }
        assert (forallb (is_open_term Γ) l''). {
          eapply closed_red_open_right in redv'.
          now rewrite PCUICOnFreeVars.on_free_vars_mkApps /= in redv'. }
        solve_all; eauto with fvs.
        constructor; eauto with fvs.
  Qed.

  Lemma closed_red_terms_open_left {Γ l l'}:
    All2 (closed_red Σ Γ) l l'
    All (is_open_term Γ) l.
  Proof using Type. solve_all; eauto with fvs. Qed.

  Lemma closed_red_terms_open_right {Γ l l'}:
    All2 (closed_red Σ Γ) l l'
    All (is_open_term Γ) l'.
  Proof using wfΣ. solve_all; eauto with fvs. Qed.
  Hint Resolve closed_red_terms_open_left closed_red_terms_open_right : fvs.

  Lemma ws_cumul_pb_terms_open_terms_left {Γ s s'} :
    ws_cumul_pb_terms Σ Γ s s'
    forallb (is_open_term Γ) s.
  Proof using wfΣ.
    solve_all; eauto with fvs.
  Qed.

  Lemma ws_cumul_pb_terms_open_terms_right {Γ s s'} :
    ws_cumul_pb_terms Σ Γ s s'
    forallb (is_open_term Γ) s'.
  Proof using wfΣ.
    solve_all; eauto with fvs.
  Qed.
  Hint Resolve ws_cumul_pb_terms_open_terms_left ws_cumul_pb_terms_open_terms_right : fvs.

  Lemma ws_cumul_pb_Ind_r_inv {pb Γ ind ui l T} :
      Σ ;;; Γ T ≤[pb] mkApps (tInd ind ui) l
       ui' l',
         Σ ;;; Γ T (mkApps (tInd ind ui') l'),
          R_global_instance Σ (eq_universe Σ) (compare_universe pb Σ) (IndRef ind) #|l| ui' ui &
          ws_cumul_pb_terms Σ Γ l' l].
  Proof using wfΣ.
    move/ws_cumul_pb_red⇒ [v [v' [redv redv' leqvv']]].
    eapply invert_red_mkApps_tInd in redv' as [l' [? ? ha]]; auto. subst.
    eapply compare_term_mkApps_r_inv in leqvv' as [u [l'' [e ? ?]]].
    subst. depelim e.
    eexists _,_. split ; eauto.
    - now rewrite (All2_length ha).
    - eapply All2_trans.
      × intros x y z h1 h2. etransitivity; tea.
      × assert (forallb (is_open_term Γ) l'). { eapply All_forallb, (All2_All_right ha); tea; eauto with fvs. }
        assert (forallb (is_open_term Γ) l''). {
          eapply closed_red_open_right in redv.
          now rewrite PCUICOnFreeVars.on_free_vars_mkApps /= in redv. }
        solve_all; eauto with fvs.
        constructor; eauto with fvs.
      × eapply All2_impl.
        + eapply All2_sym; tea.
        + cbn. eauto with pcuic.
  Qed.

  Lemma ws_cumul_pb_Ind_inv {pb Γ ind ind' ui ui' l l'} :
      Σ ;;; Γ mkApps (tInd ind ui) l ≤[pb] mkApps (tInd ind' ui') l'
       ind = ind',
         R_global_instance Σ (eq_universe Σ) (compare_universe pb Σ) (IndRef ind) #|l| ui ui',
         is_closed_context Γ & ws_cumul_pb_terms Σ Γ l l'].
  Proof using wfΣ.
    move/ws_cumul_pb_red⇒ [v [v' [redv redv' leqvv']]].
    pose proof (clrel_ctx redv).
    eapply invert_red_mkApps_tInd in redv as [l0 [? ? ha]]; auto. subst.
    eapply invert_red_mkApps_tInd in redv' as [l1 [? ? ha']]; auto. subst.
    eapply compare_term_mkApps_l_inv in leqvv' as [u [l'' [e ? ?]]].
    depelim e; solve_discr.
    noconf H0. noconf H1. split ⇒ //.
    + now rewrite (All2_length ha).
    + eapply red_terms_ws_cumul_pb_terms in ha.
      eapply red_terms_ws_cumul_pb_terms in ha'.
      eapply eq_terms_ws_cumul_pb_terms in a; tea; fvs.
      transitivity l0 ⇒ //. transitivity l1 ⇒ //. now symmetry.
  Qed.

End Inversions.

#[global] Hint Resolve closed_red_terms_open_left closed_red_terms_open_right : fvs.
#[global] Hint Resolve ws_cumul_pb_terms_open_terms_left ws_cumul_pb_terms_open_terms_right : fvs.


Injectivity of products, the essential property of cumulativity needed for subject reduction.
Lemma cumul_Prod_inv {cf:checker_flags} {Σ : global_env_ext} {wfΣ : wf Σ} {Γ na na' A B A' B'} :
  Σ ;;; Γ tProd na A B tProd na' A' B'
   eq_binder_annot na na', Σ ;;; Γ A = A' & Σ ;;; Γ ,, vass na' A' B B']%type.
Proof.
  intros H.
  now eapply ws_cumul_pb_Prod_Prod_inv in H.
Qed.

Injectivity of products for conversion holds as well
Lemma conv_Prod_inv {cf:checker_flags} {Σ : global_env_ext} {wfΣ : wf Σ} {Γ na na' A B A' B'} :
  Σ ;;; Γ tProd na A B = tProd na' A' B'
   eq_binder_annot na na', Σ ;;; Γ A = A' & (Σ ;;; Γ ,, vass na' A' B = B')]%type.
Proof.
  intros H.
  now eapply ws_cumul_pb_Prod_Prod_inv in H.
Qed.

Lemma tProd_it_mkProd_or_LetIn na A B ctx s :
  tProd na A B = it_mkProd_or_LetIn ctx (tSort s)
  { ctx' & ctx = (ctx' ++ [vass na A])
           destArity [] B = Some (ctx', s) }.
Proof.
  intros. (removelast ctx).
  revert na A B s H.
  induction ctx using rev_ind; intros; noconf H.
  rewrite it_mkProd_or_LetIn_app in H. simpl in H.
  destruct x as [na' [b'|] ty']; noconf H; simpl in ×.
  rewrite removelast_app. 1: congruence.
  simpl. rewrite app_nil_r. intuition auto.
  rewrite destArity_it_mkProd_or_LetIn. simpl. now rewrite app_context_nil_l.
Qed.

Definition ws_cumul_pb_predicate {cf} Σ Γ p p' :=
   ws_cumul_pb_terms Σ Γ p.(pparams) p'.(pparams),
     R_universe_instance (eq_universe Σ) (puinst p) (puinst p'),
     eq_context_gen eq eq (pcontext p) (pcontext p') &
     Σ ;;; Γ ,,, inst_case_predicate_context p preturn p = preturn p'].

Definition ws_cumul_pb_brs {cf} Σ Γ p :=
  All2 (fun br br'
    eq_context_gen eq eq (bcontext br) (bcontext br') ×
    Σ ;;; Γ ,,, inst_case_branch_context p br bbody br = bbody br').

Section Inversions.
  Context {cf : checker_flags} {Σ : global_env_ext} {wfΣ : wf Σ}.

  Lemma ws_cumul_pb_App_l {pb Γ f f' u} :
    Σ ;;; Γ f ≤[pb] f'
    is_open_term Γ u
    Σ ;;; Γ tApp f u ≤[pb] tApp f' u.
  Proof using wfΣ.
    intros h onu.
    induction h.
    - constructor; cbn; eauto with fvs. cbn in c.
      destruct pb; constructor; eauto with fvs; try reflexivity.
      + eapply leq_term_leq_term_napp; tc; tas.
      + apply eq_term_eq_term_napp; tc; tas.
    - eapply red_ws_cumul_pb_left; tea.
      econstructor; tea; cbn; eauto with fvs.
      eapply red1_red. constructor; auto.
    - eapply red_ws_cumul_pb_right; tea.
      econstructor; tea; cbn; eauto with fvs.
      eapply red1_red. constructor; auto.
  Qed.

  Lemma ws_cumul_pb_App_r {pb Γ f u v} :
    is_open_term Γ f
    Σ ;;; Γ u = v
    Σ ;;; Γ tApp f u ≤[pb] tApp f v.
  Proof using wfΣ.
    intros onf h.
    induction h.
    - constructor; cbn; eauto with fvs. cbn in c.
      destruct pb; constructor; eauto with fvs; reflexivity.
    - eapply red_ws_cumul_pb_left; tea.
      econstructor; tea; cbn; eauto with fvs.
      eapply red1_red. constructor; auto.
    - eapply red_ws_cumul_pb_right; tea.
      econstructor; tea; cbn; eauto with fvs.
      eapply red1_red. constructor; auto.
  Qed.

  Lemma ws_cumul_pb_mkApps {pb Γ hd args hd' args'} :
    Σ;;; Γ hd ≤[pb] hd'
   ws_cumul_pb_terms Σ Γ args args'
    Σ;;; Γ mkApps hd args ≤[pb] mkApps hd' args'.
  Proof using wfΣ.
    intros cum cum_args.
    revert hd hd' cum.
    induction cum_args; intros hd hd' cum; auto.
    cbn.
    apply IHcum_args.
    etransitivity.
    - eapply ws_cumul_pb_App_l; tea; eauto with fvs.
    - eapply ws_cumul_pb_App_r; eauto with fvs.
  Qed.

  Notation "Σ ;;; Γ ⊢ t ⇝1 u" := (closed_red1 Σ Γ t u) (at level 50, Γ, t, u at next level,
  format "Σ ;;; Γ ⊢ t ⇝1 u").

  Lemma closed_red1_mkApps_left {Γ} {t u ts} :
    Σ ;;; Γ t ⇝1 u
    forallb (is_open_term Γ) ts
    Σ ;;; Γ mkApps t ts ⇝1 mkApps u ts.
  Proof using Type.
    intros r cl.
    split; eauto with fvs.
    - rewrite on_free_vars_mkApps (clrel_src r) //.
    - eapply red1_mkApps_f, r.
  Qed.


  Lemma invert_cumul_prod_ind {Γ na dom codom ind u args} :
    Σ ;;; Γ tProd na dom codom mkApps (tInd ind u) args False.
  Proof using wfΣ.
    intros ht; eapply ws_cumul_pb_Prod_l_inv in ht as (? & ? & ? & []); auto.
    eapply invert_red_mkApps_tInd in c as (? & []); auto. solve_discr.
  Qed.

  Lemma invert_cumul_ind_prod {Γ na dom codom ind u args} :
    Σ ;;; Γ mkApps (tInd ind u) args tProd na dom codom False.
  Proof using wfΣ.
    intros ht; eapply ws_cumul_pb_Prod_r_inv in ht as (? & ? & ? & []); auto.
    eapply invert_red_mkApps_tInd in c as (? & []); auto. solve_discr.
    Qed.

  Lemma invert_cumul_ind_ind {Γ ind ind' u u' args args'} :
    Σ ;;; Γ mkApps (tInd ind u) args mkApps (tInd ind' u') args'
    (eqb ind ind' × PCUICEquality.R_global_instance Σ (eq_universe Σ) (leq_universe Σ) (IndRef ind) #|args| u u' ×
      ws_cumul_pb_terms Σ Γ args args').
  Proof using wfΣ.
    intros ht; eapply ws_cumul_pb_Ind_l_inv in ht as (? & ? & [? ? ?]); auto.
    eapply invert_red_mkApps_tInd in c as (? & [? ? ?]); auto; solve_discr. noconf H.
    subst x1. intuition auto.
    - eapply eq_inductive_refl.
    - transitivity x0; auto. symmetry. now eapply red_terms_ws_cumul_pb_terms.
  Qed.

  Lemma invert_cumul_sort_ind {Γ s ind u args} :
    Σ;;; Γ tSort s mkApps (tInd ind u) args False.
  Proof using wfΣ.
    intros cum.
    apply PCUICConversion.ws_cumul_pb_Sort_l_inv in cum as (?&?&?).
    apply invert_red_mkApps_tInd in c as (?&[]); auto.
    solve_discr.
  Qed.

  Lemma invert_cumul_ind_sort {Γ s ind u args} :
    Σ;;; Γ mkApps (tInd ind u) args tSort s False.
  Proof using wfΣ.
    intros cum.
    apply PCUICConversion.ws_cumul_pb_Sort_r_inv in cum as (?&?&?).
    apply invert_red_mkApps_tInd in c as (?&[]); auto.
    solve_discr.
  Qed.

End Inversions.


Definition sq_ws_cumul_pb {cf : checker_flags} pb Σ Γ T U := Σ ;;; Γ T ≤[pb] U .

Section ConvRedConv.

  Context {cf : checker_flags}.
  Context {Σ : global_env_ext} {wfΣ : wf Σ}.

  Lemma conv_red_conv Γ Γ' t tr t' t'r :
    Σ Γ = Γ'
    Σ ;;; Γ t tr
    Σ ;;; Γ' t' t'r
    Σ ;;; Γ tr = t'r
    Σ ;;; Γ t = t'.
  Proof using wfΣ.
    intros cc r r' ct.
    eapply red_ws_cumul_pb_left; eauto.
    eapply ws_cumul_pb_ws_cumul_ctx in ct.
    2:symmetry; tea.
    eapply ws_cumul_pb_ws_cumul_ctx; tea.
    eapply red_ws_cumul_pb_right; tea.
  Qed.

  Lemma Prod_conv_cum_inv {Γ leq na1 na2 A1 A2 B1 B2} :
    sq_ws_cumul_pb leq Σ Γ (tProd na1 A1 B1) (tProd na2 A2 B2)
      eq_binder_annot na1 na2 Σ ;;; Γ A1 = A2
      sq_ws_cumul_pb leq Σ (Γ,, vass na1 A1) B1 B2.
  Proof using wfΣ.
    intros [].
    apply ws_cumul_pb_Prod_Prod_inv in X as []; intuition auto; sq; auto.
    eapply (ws_cumul_pb_ws_cumul_ctx (pb':=Conv)) in w0; tea.
    constructor; auto.
    - apply ws_cumul_ctx_pb_refl; eauto with fvs.
    - constructor; auto.
  Qed.

  Lemma conv_cum_conv_ctx leq pb Γ Γ' T U :
    sq_ws_cumul_pb leq Σ Γ T U
    Σ Γ' ≤[pb] Γ
    sq_ws_cumul_pb leq Σ Γ' T U.
  Proof using wfΣ.
    intros [] h.
    now eapply ws_cumul_pb_ws_cumul_ctx in X; tea.
  Qed.

  Lemma conv_cum_red leq Γ t1 t2 t1' t2' :
    Σ ;;; Γ t1' t1
    Σ ;;; Γ t2' t2
    sq_ws_cumul_pb leq Σ Γ t1 t2
    sq_ws_cumul_pb leq Σ Γ t1' t2'.
  Proof using wfΣ.
    intros r1 r2 [cc]. sq.
    eapply red_ws_cumul_pb_left; tea.
    eapply red_ws_cumul_pb_right; tea.
  Qed.

  Lemma conv_cum_red_conv leq Γ Γ' t1 t2 t1' t2' :
    Σ Γ = Γ'
    Σ ;;; Γ t1' t1
    Σ ;;; Γ' t2' t2
    sq_ws_cumul_pb leq Σ Γ t1 t2
    sq_ws_cumul_pb leq Σ Γ t1' t2'.
  Proof using wfΣ.
    intros conv_ctx r1 r2 [cc]; sq.
    eapply red_ws_cumul_pb_left; tea.
    eapply ws_cumul_pb_ws_cumul_ctx in cc; tea. 2:symmetry; tea.
    eapply ws_cumul_pb_ws_cumul_ctx; tea.
    eapply red_ws_cumul_pb_right; tea.
  Qed.

  Lemma conv_cum_red_inv leq Γ t1 t2 t1' t2' :
    Σ ;;; Γ t1 t1'
    Σ ;;; Γ t2 t2'
    sq_ws_cumul_pb leq Σ Γ t1 t2
    sq_ws_cumul_pb leq Σ Γ t1' t2'.
  Proof using wfΣ.
    intros r1 r2 [cc]; sq.
    transitivity t1.
    - now eapply red_ws_cumul_pb_inv.
    - transitivity t2 ⇒ //.
      now apply red_ws_cumul_pb.
  Qed.

  Lemma conv_cum_red_conv_inv pb Γ Γ' t1 t2 t1' t2' :
    Σ Γ = Γ'
    Σ ;;; Γ t1 t1'
    Σ ;;; Γ' t2 t2'
    sq_ws_cumul_pb pb Σ Γ t1 t2
    sq_ws_cumul_pb pb Σ Γ t1' t2'.
  Proof using wfΣ.
    moveconv_ctx r1 /(red_ws_cumul_pb (pb:=pb)) r2 [cc]; sq.
    transitivity t1; [now apply red_ws_cumul_pb_inv|].
    transitivity t2 ⇒ //.
    eapply ws_cumul_pb_ws_cumul_ctx in r2; tea.
  Qed.

  Lemma conv_cum_red_iff leq Γ t1 t2 t1' t2' :
    Σ ;;; Γ t1' t1
    Σ ;;; Γ t2' t2
    sq_ws_cumul_pb leq Σ Γ t1 t2 sq_ws_cumul_pb leq Σ Γ t1' t2'.
  Proof using wfΣ.
    intros r1 r2.
    split; intros cc.
    - eapply conv_cum_red; eauto.
    - eapply conv_cum_red_inv; eauto.
  Qed.

  Lemma conv_cum_red_conv_iff pb Γ Γ' t1 t2 t1' t2' :
    Σ Γ = Γ'
    Σ ;;; Γ t1' t1
    Σ ;;; Γ' t2' t2
    sq_ws_cumul_pb pb Σ Γ t1 t2 sq_ws_cumul_pb pb Σ Γ t1' t2'.
  Proof using wfΣ.
    intros conv_ctx r1 r2.
    split; intros cc.
    - eapply conv_cum_red_conv; eauto.
    - eapply conv_cum_red_conv_inv; eauto.
  Qed.


  Lemma ws_cumul_pb_Proj_c {pb Γ p u v} :
    Σ ;;; Γ u = v
    Σ ;;; Γ tProj p u ≤[pb] tProj p v.
  Proof using wfΣ.
    intros h.
    induction h.
    - eapply ws_cumul_pb_compare; eauto.
      destruct pb; constructor; assumption.
    - transitivity (tProj p v) ⇒ //.
      eapply red_ws_cumul_pb. constructor; eauto with fvs.
      econstructor. constructor. assumption.
    - transitivity (tProj p v) ⇒ //.
      eapply red_ws_cumul_pb_inv. constructor; eauto with fvs.
      econstructor. constructor. assumption.
  Qed.

  Lemma ws_cumul_pb_App :
     Γ t1 t2 u1 u2 pb,
      Σ ;;; Γ t1 ≤[pb] t2
      Σ ;;; Γ u1 = u2
      Σ ;;; Γ tApp t1 u1 ≤[pb] tApp t2 u2.
  Proof using wfΣ.
    intros. etransitivity.
    - eapply ws_cumul_pb_App_l; tea; eauto with fvs.
    - apply ws_cumul_pb_App_r; tea. eauto with fvs.
  Qed.

  #[global]
  Instance all_eq_term_refl : Reflexive (All2 (eq_term_upto_univ Σ.1 (eq_universe Σ) (eq_universe Σ))).
  Proof using Type.
    intros x. apply All2_same. intros. reflexivity.
  Qed.

  Definition set_puinst (p : predicate term) (puinst : Instance.t) : predicate term :=
    {| pparams := p.(pparams);
        puinst := puinst;
        pcontext := p.(pcontext);
        preturn := p.(preturn) |}.

  Definition set_preturn_two {p} pret pret' : set_preturn (set_preturn p pret') pret = set_preturn p pret :=
    eq_refl.


  Notation is_open_brs Γ p brs :=
    (forallb (fun br : branch term
      test_context_k (fun k : naton_free_vars (closedP k xpredT)) #|pparams p| (bcontext br) &&
      on_free_vars (shiftnP #|bcontext br| (shiftnP #|Γ| xpred0)) (bbody br)) brs).

  Notation is_open_predicate Γ p :=
    ([&& forallb (is_open_term Γ) p.(pparams),
    on_free_vars (shiftnP #|p.(pcontext)| (shiftnP #|Γ| xpred0)) p.(preturn) &
    test_context_k (fun k : naton_free_vars (closedP k xpredT)) #|p.(pparams)| p.(pcontext)]).


  Lemma All2_many_OnOne2_pres {A} (R : A A Type) (P : A Type) l l' :
    All2 R l l'
    ( x y, R x y P x × P y)
    rtrans_clos (fun x y#|x| = #|y| × OnOne2 R x y × All P x × All P y) l l'.
  Proof using Type.
    intros h H.
    induction h.
    - constructor.
    - econstructor.
      + split; revgoals.
        × split.
          { constructor; tea. }
          pose proof (All2_impl h H).
          eapply All2_prod_inv in X as [Hl Hl'].
          eapply All2_All_left in Hl; eauto.
          eapply All2_All_right in Hl'; eauto.
          specialize (H _ _ r) as [].
          constructor; constructor; auto.
        × now cbn.
      + pose proof (All2_impl h H).
        eapply All2_prod_inv in X as [Hl Hl'].
        eapply All2_All_left in Hl; eauto.
        eapply All2_All_right in Hl'; eauto.
        specialize (H _ _ r) as [].
        clear -IHh Hl Hl' p p0. rename IHh into h.
        induction h.
        × constructor.
        × destruct r as [hlen [onz [py pz]]].
          econstructor.
          -- split; revgoals. 1:split.
            { econstructor 2; tea. }
            { split; constructor; auto. }
            now cbn.
          -- now apply IHh.
  Qed.

  Lemma rtrans_clos_length {A} {l l' : list A} {P} :
    rtrans_clos (fun x y : list A#|x| = #|y| × P x y) l l' #|l| = #|l'|.
  Proof using Type.
    induction 1; auto.
    destruct r.
    now transitivity #|y|.
  Qed.

  Definition is_open_case (Γ : context) p c brs :=
    [&& forallb (is_open_term Γ) p.(pparams),
    on_free_vars (shiftnP #|p.(pcontext)| (shiftnP #|Γ| xpred0)) p.(preturn),
    test_context_k (fun k : naton_free_vars (closedP k xpredT)) #|p.(pparams)| p.(pcontext),
    is_open_term Γ c & is_open_brs Γ p brs].

  Lemma is_open_case_split {Γ p c brs} : is_open_case Γ p c brs =
    [&& is_open_predicate Γ p, is_open_term Γ c & is_open_brs Γ p brs].
  Proof using Type.
    rewrite /is_open_case. now repeat bool_congr.
  Qed.

  Lemma is_open_case_set_pparams Γ p c brs pars' :
    forallb (is_open_term Γ) pars'
    #|pars'| = #|p.(pparams)|
    is_open_case Γ p c brs
    is_open_case Γ (set_pparams p pars') c brs.
  Proof using Type.
    moveonpars' Hlen.
    move/and5P ⇒ [] onpars.
    rewrite /is_open_case ⇒ →.
    rewrite -Hlen ⇒ → → → /=.
    rewrite andb_true_r //.
  Qed.

  Lemma is_open_case_set_preturn Γ p c brs pret' :
    is_open_term (Γ ,,, inst_case_predicate_context p) pret'
    is_open_case Γ p c brs
    is_open_case Γ (set_preturn p pret') c brs.
  Proof using Type.
    moveonpret' /and5P[] onpars onpret onpctx onc onbrs.
    rewrite /is_open_case onc onbrs !andb_true_r onpctx /= onpars /= andb_true_r.
    rewrite app_length inst_case_predicate_context_length in onpret'.
    now rewrite shiftnP_add.
  Qed.

  Instance red_brs_refl p Γ : Reflexive (@red_brs Σ p Γ).
  Proof using Type. intros x. eapply All2_refl; split; reflexivity. Qed.

  Instance red_terms_refl Γ : Reflexive (All2 (red Σ Γ)).
  Proof using Type. intros x; eapply All2_refl; reflexivity. Qed.

  Instance eqbrs_refl : Reflexive (All2 (fun x y : branch term
      eq_context_gen eq eq (bcontext x) (bcontext y) ×
      eq_term_upto_univ Σ.1 (eq_universe Σ) (eq_universe Σ) (bbody x) (bbody y))).
  Proof using Type. intros brs; eapply All2_refl; split; reflexivity. Qed.

  Lemma ws_cumul_pb_Case_p {Γ ci c brs p p'} :
    is_closed_context Γ
    is_open_case Γ p c brs
    is_open_predicate Γ p'
    ws_cumul_pb_predicate Σ Γ p p'
    Σ ;;; Γ tCase ci p c brs = tCase ci p' c brs.
  Proof using wfΣ.
    intros onΓ oncase onp' [cpars cu cctx cret].
    assert (Σ ;;; Γ tCase ci p c brs = tCase ci (set_preturn p (preturn p')) c brs).
    { eapply ws_cumul_pb_red in cret as [v [v' [redl redr eq]]].
      eapply ws_cumul_pb_red.
       (tCase ci (set_preturn p v) c brs).
       (tCase ci (set_preturn p v') c brs).
      repeat split; auto.
      - cbn. eapply red_case; try reflexivity.
         apply redl.
      - apply is_open_case_set_preturn ⇒ //; eauto with fvs.
      - rewrite -[set_preturn _ v'](set_preturn_two _ (preturn p')).
        eapply red_case; try reflexivity.
        cbn. apply redr.
      - constructor; try reflexivity.
        repeat split; try reflexivity.
        cbn. apply eq. }
    etransitivity; tea.
    set (pret := set_preturn p (preturn p')).
    assert (Σ ;;; Γ tCase ci pret c brs = tCase ci (set_puinst pret (puinst p')) c brs).
    { constructor. 1:eauto with fvs. 1:eauto with fvs.
      { eapply ws_cumul_pb_is_open_term_right in X. apply X. }
      econstructor; try reflexivity.
      red; intuition try reflexivity. }
    etransitivity; tea.
    set (ppuinst := set_puinst pret (puinst p')) in ×.
    assert (Σ ;;; Γ tCase ci ppuinst c brs = tCase ci (set_pparams ppuinst p'.(pparams)) c brs).
    { apply ws_cumul_pb_is_open_term_right in X0.
      clear -wfΣ cctx cpars onΓ X0.
      eapply All2_many_OnOne2_pres in cpars.
      2:{ intros x y conv. split.
          1:eapply ws_cumul_pb_is_open_term_left; tea. eauto with fvs. }
      clear cctx.
      induction cpars.
      × eapply ws_cumul_pb_compare; tea.
        destruct p; cbn. reflexivity.
      × destruct r as [hlen [onr [axy az]]].
        transitivity (tCase ci (set_pparams ppuinst y) c brs) ⇒ //.
        eapply OnOne2_split in onr as [? [? [? [? [conv [-> ->]]]]]].
        eapply ws_cumul_pb_red in conv as [v [v' [redl redr eq]]].
        apply ws_cumul_pb_red.
         (tCase ci (set_pparams ppuinst (x1 ++ v :: x2)) c brs).
         (tCase ci (set_pparams ppuinst (x1 ++ v' :: x2)) c brs).
        split.
        { constructor; auto.
          { eapply All_forallb in axy.
            eapply is_open_case_set_pparams ⇒ //.
            now apply rtrans_clos_length in cpars. }
          rewrite -[set_pparams _ (x1 ++ v :: _)](set_pparams_two (x1 ++ x :: x2)).
          eapply red_case; try reflexivity.
          { cbn. eapply All2_app.
            { eapply All2_refl. reflexivity. }
            constructor; [apply redl|].
            eapply All2_refl; reflexivity. } }
        { constructor; auto.
          { eapply All_forallb in az.
            eapply is_open_case_set_pparams ⇒ //.
            apply rtrans_clos_length in cpars.
            now rewrite !app_length /= in cpars ×. }
          rewrite -[set_pparams _ (x1 ++ v' :: _)](set_pparams_two (x1 ++ x0 :: x2)).
          eapply red_case; try reflexivity.
          { cbn. eapply All2_app; try reflexivity.
            constructor; [apply redr|]; reflexivity. } }
        cbn; constructor; try reflexivity.
        repeat split; try reflexivity.
        cbn. eapply All2_app; try reflexivity.
        constructor ⇒ //; reflexivity. }
    etransitivity; tea.
    apply into_ws_cumul_pb; auto.
    { destruct p'; cbn in *; unfold set_pparams, ppuinst, pret; cbn.
      repeat constructor; cbn; try reflexivity; tas. }
    1:eauto with fvs.
    cbn.
    move/and3P: onp' ⇒ [] → → → /=.
    move/and5P: oncase ⇒ [] _ _ _ → /=.
    now rewrite (All2_length cpars).
  Qed.

  Lemma ws_cumul_pb_Case_c :
     Γ indn p brs u v,
      is_open_predicate Γ p
      is_open_brs Γ p brs
      Σ ;;; Γ u = v
      Σ ;;; Γ tCase indn p u brs = tCase indn p v brs.
  Proof using wfΣ.
    intros Γ ci p brs u v onp onbrs h.
    induction h.
    - constructor; auto with fvs.
      + rewrite [is_open_term _ _]is_open_case_split onp onbrs !andb_true_r /= //.
      + rewrite [is_open_term _ _]is_open_case_split onp onbrs !andb_true_r /= //.
      + cbn. constructor; auto; try reflexivity.
    - eapply red_ws_cumul_pb_left ; eauto.
      eapply into_closed_red; tea.
      { constructor. constructor. assumption. }
      rewrite [is_open_term _ _]is_open_case_split onp onbrs /= andb_true_r //.
    - eapply red_ws_cumul_pb_right; tea.
      constructor; pcuic.
      rewrite [is_open_term _ _]is_open_case_split onp onbrs /= andb_true_r //.
  Qed.

  Lemma eq_context_gen_subst_context :
     u v n k,
      eq_context_gen eq eq u v
      eq_context_gen eq eq (subst_context n k u) (subst_context n k v).
  Proof using Type.
    intros re u v n.
    induction 1.
    - constructor.
    - rewrite !subst_context_snoc; constructor; eauto.
      depelim p; constructor; simpl; intuition auto; subst;
      rewrite -(length_of X); auto.
  Qed.

  Lemma eq_context_gen_inst_case_context {Γ Δ Δ' pars puinst} :
    eq_context_gen eq eq Δ Δ'
    eq_context_gen eq eq (Γ ,,, inst_case_context pars puinst Δ) (Γ ,,, inst_case_context pars puinst Δ').
  Proof using Type.
    intros.
    apply All2_fold_app; [reflexivity|].
    rewrite /inst_case_context.
    now eapply eq_context_gen_subst_context, eq_context_gen_eq_univ_subst_preserved.
  Qed.

  Lemma ws_cumul_pb_Case_one_brs {Γ indn p c brs brs'} :
    is_closed_context Γ
    is_open_predicate Γ p
    is_open_term Γ c
    is_open_brs Γ p brs
    is_open_brs Γ p brs'
    OnOne2 (fun u v
      eq_context_gen eq eq u.(bcontext) v.(bcontext) ×
      Σ ;;; (Γ ,,, inst_case_branch_context p u) u.(bbody) = v.(bbody)) brs brs'
    Σ ;;; Γ tCase indn p c brs = tCase indn p c brs'.
  Proof using wfΣ.
    intros onΓ onp onc onbrs onbrs' h.
    apply OnOne2_split in h as [[bctx br] [[m' br'] [l1 [l2 [[? h] [? ?]]]]]].
    simpl in ×. subst brs brs'.
    induction h.
    × constructor ⇒ //.
      + rewrite [is_open_term _ _]is_open_case_split onp onc /=.
        move: onbrs i0.
        rewrite !forallb_app ⇒ /andP[] → /= /andP[] ⇒ /andP[] ⇒ → /= _ →.
        now rewrite andb_true_r shiftnP_add app_length inst_case_branch_context_length /=.
      + rewrite [is_open_term _ _]is_open_case_split onp onc /=.
        move: onbrs' i1.
        rewrite !forallb_app ⇒ /andP[] → /= /andP[] ⇒ /andP[] ⇒ → /= _ →.
        now rewrite andb_true_r shiftnP_add app_length inst_case_branch_context_length /= -(All2_fold_length a).
      + constructor; try reflexivity.
        eapply All2_app; try reflexivity.
        constructor; try split; try reflexivity; cbn ⇒ //.
    × eapply red_ws_cumul_pb_left; tea.
      2:{ eapply IHh ⇒ //. }
      eapply into_closed_red; eauto.
      { constructor. constructor.
        eapply OnOne2_app. constructor; auto. }
      rewrite [is_open_term _ _]is_open_case_split onp onc /=.
      move: onbrs i0.
      rewrite !forallb_app ⇒ /andP[] → /= /andP[] ⇒ /andP[] ⇒ → /= _ →.
      now rewrite andb_true_r shiftnP_add app_length inst_case_branch_context_length /=.
    × eapply red_ws_cumul_pb_right; tea.
      2:{ eapply IHh ⇒ //.
          move: onbrs' i2.
          rewrite !forallb_app ⇒ /andP[] → /= /andP[] ⇒ /andP[] ⇒ → /= _ →.
          now rewrite andb_true_r shiftnP_add app_length inst_case_branch_context_length /= (All2_fold_length a). }
      eapply into_closed_red; eauto ⇒ //.
      { constructor. constructor.
        eapply OnOne2_app. constructor; auto. cbn. split; auto.
        eapply red1_eq_context_upto_names; tea.
        rewrite /inst_case_branch_context /=.
        now eapply eq_context_upto_names_gen, eq_context_gen_inst_case_context. }
      rewrite [is_open_term _ _]is_open_case_split onp onc /= //.
  Qed.

  Lemma is_open_brs_OnOne2 Γ p x y :
    is_open_brs Γ p x
    OnOne2 (fun u v : branch term
      eq_context_gen eq eq (bcontext u) (bcontext v) ×
      (Σ ;;; Γ,,, inst_case_branch_context p u bbody u = bbody v)) y x
    is_open_brs Γ p y.
  Proof using wfΣ.
    intros op.
    induction 1.
    - cbn. destruct p0 as [e e0].
      move: op ⇒ /= /andP[] /andP[] cl clb →.
      rewrite andb_true_r /=. apply/andP; split.
      2:{ eapply ws_cumul_pb_is_open_term_left in e0.
        rewrite app_length inst_case_branch_context_length in e0.
        now rewrite shiftnP_add. }
      rewrite !test_context_k_closed_on_free_vars_ctx in cl ×.
      eapply eq_context_upto_names_on_free_vars; tea.
      eapply eq_context_upto_names_gen.
      now symmetry.
    - now move: op ⇒ /= /andP[] ⇒ →.
  Qed.

  Lemma ws_cumul_pb_Case_brs {Γ ci p c brs brs'} :
    is_closed_context Γ
    is_open_predicate Γ p
    is_open_term Γ c
    is_open_brs Γ p brs
    is_open_brs Γ p brs'
    ws_cumul_pb_brs Σ Γ p brs brs'
    Σ ;;; Γ tCase ci p c brs = tCase ci p c brs'.
  Proof using wfΣ.
    intros onΓ onp onc onbrs onbrs' h.
    eapply (All2_many_OnOne2_pres _ (fun br
      is_open_term (Γ ,,, inst_case_branch_context p br) br.(bbody))) in h.
    2:{ intros x y [eq cv].
        split; [eapply ws_cumul_pb_is_open_term_left|eapply ws_cumul_pb_is_open_term_right]; tea.
        instantiate (1:=bbody x). instantiate (1 := Conv).
        eapply ws_cumul_pb_eq_context_upto; tea.
        { eapply eq_context_gen_eq_context_upto; tc.
          now eapply eq_context_gen_inst_case_context. }
        eapply ws_cumul_pb_is_closed_context in cv.
        eapply eq_context_upto_names_on_free_vars; tea.
        eapply eq_context_upto_names_gen.
        now eapply eq_context_gen_inst_case_context. }
    induction h.
    - apply ws_cumul_pb_compare; tas.
      1-2:rewrite [is_open_term _ _]is_open_case_split onp onc /= //.
      cbn; reflexivity.
    - destruct r as [o [ony onz]].
      etransitivity.
      + apply IHh.
        eapply is_open_brs_OnOne2; tea.
      + apply ws_cumul_pb_Case_one_brs; tea.
        eapply is_open_brs_OnOne2; tea.
  Qed.

  Lemma ws_cumul_pb_Case {Γ ci p p' c c' brs brs'} :
    is_open_case Γ p c brs
    is_open_case Γ p' c' brs'
    ws_cumul_pb_predicate Σ Γ p p'
    Σ ;;; Γ c = c'
    ws_cumul_pb_brs Σ Γ p brs brs'
    Σ ;;; Γ tCase ci p c brs = tCase ci p' c' brs'.
  Proof using wfΣ.
    intros onc0. generalize onc0.
    rewrite !is_open_case_split ⇒ /and3P[onp onc onbrs] /and3P[onp' onc' onbrs'].
    movecvp cvc.
    assert (clΓ := ws_cumul_pb_is_closed_context cvc).
    etransitivity.
    { eapply ws_cumul_pb_Case_brs. 6:tea. all:tas.
      destruct cvp as [onpars oninst onctx onr].
      now rewrite (All2_length onpars). }
    etransitivity.
    { eapply ws_cumul_pb_Case_c; tea.
      destruct cvp as [onpars oninst onctx onr].
      now rewrite (All2_length onpars). }
    eapply ws_cumul_pb_Case_p; tea.
    destruct cvp as [onpars oninst onctx onr].
    rewrite is_open_case_split onp onc' /=.
    now rewrite (All2_length onpars).
  Qed.

  Definition fix_or_cofix b mfix idx :=
    (if b then tFix else tCoFix) mfix idx.

   Lemma eq_term_fix_or_cofix b mfix idx mfix' :
     All2 (fun x y : def term
       ((eq_term_upto_univ Σ.1 (eq_universe Σ) (eq_universe Σ) (dtype x) (dtype y)
        × eq_term_upto_univ Σ.1 (eq_universe Σ) (eq_universe Σ) (dbody x) (dbody y)) × rarg x = rarg y) ×
      eq_binder_annot (dname x) (dname y)) mfix mfix'
    eq_term Σ Σ (fix_or_cofix b mfix idx) (fix_or_cofix b mfix' idx).
  Proof using Type.
    destruct b; constructor; auto.
  Qed.

  Notation is_open_def Γ n :=
    (test_def (on_free_vars (shiftnP #|Γ| xpred0)) (on_free_vars (shiftnP n (shiftnP #|Γ| xpred0)))).

  Notation is_open_mfix Γ mfix :=
    (forallb (is_open_def Γ #|mfix|) mfix).

  Lemma is_open_fix_or_cofix {b} {Γ : context} {mfix idx} :
    is_open_term Γ (fix_or_cofix b mfix idx) =
    is_open_mfix Γ mfix.
  Proof using Type. by case: b. Qed.

  Lemma ws_cumul_pb_fix_one_type {b Γ mfix mfix' idx} :
    is_closed_context Γ
    is_open_mfix Γ mfix
    is_open_mfix Γ mfix'
    OnOne2 (fun u v
      Σ ;;; Γ dtype u = dtype v ×
      dbody u = dbody v ×
      (rarg u = rarg v) ×
      eq_binder_annot (dname u) (dname v)
    ) mfix mfix'
    Σ ;;; Γ fix_or_cofix b mfix idx = fix_or_cofix b mfix' idx.
  Proof using wfΣ.
    intros onΓ onmfix onmfix' h.
    eapply into_ws_cumul_pb ⇒ //; rewrite ?is_open_fix_or_cofix //.
    clear onmfix onmfix'.
    apply OnOne2_split in h
      as [[na ty bo ra] [[na' ty' bo' ra'] [l1 [l2 [[h [? ?]] [? ?]]]]]].
    simpl in ×. subst. destruct p as [eqra eqna]. subst.
    induction h.
    - constructor; tea.
      apply eq_term_fix_or_cofix.
      apply All2_app.
      × apply All2_same. intros. intuition reflexivity.
      × constructor.
        { simpl. intuition reflexivity. }
        apply All2_same. intros. intuition reflexivity.
    - eapply cumul_red_l; eauto.
      destruct b; constructor; eapply OnOne2_app;
      constructor; cbn; intuition eauto.
    - eapply cumul_red_r ; eauto.
      destruct b; constructor; apply OnOne2_app; constructor; simpl;
      intuition eauto.
  Qed.

  Lemma ws_cumul_pb_fix_types {b Γ mfix mfix' idx} :
    is_closed_context Γ
    is_open_mfix Γ mfix
    is_open_mfix Γ mfix'
    All2 (fun u v
      Σ ;;; Γ dtype u = dtype v ×
      dbody u = dbody v ×
      (rarg u = rarg v) ×
      (eq_binder_annot (dname u) (dname v)))
      mfix mfix'
    Σ ;;; Γ fix_or_cofix b mfix idx = fix_or_cofix b mfix' idx.
  Proof using wfΣ.
    intros onΓ onm onm' h.
    pose proof onm.
    cbn in onm, onm'.
    eapply forallb_All in onm.
    eapply forallb_All in onm'.
    eapply All2_All_mix_left in h; tea.
    eapply All2_All_mix_right in h; tea.
    eapply (All2_many_OnOne2_pres _ (is_open_def Γ #|mfix|)) in h.
    2:{ intuition auto. now rewrite (All2_length h). }
    induction h.
    - constructor ⇒ //.
      1-2:rewrite is_open_fix_or_cofix //.
      cbn; reflexivity.
    - etransitivity.
      + eapply IHh.
      + destruct r as [hlen [onone [ay az]]].
        eapply ws_cumul_pb_fix_one_type; tea; solve_all.
        all:now rewrite -?hlen -(rtrans_clos_length h).
  Qed.

  Lemma red_fix_or_cofix_body b (Γ : context) (mfix : mfixpoint term) (idx : nat) (mfix' : list (def term)) :
    All2 (on_Trel_eq (red Σ (Γ,,, fix_context mfix)) dbody
      (fun x0 : def term(dname x0, dtype x0, rarg x0))) mfix mfix'
    red Σ Γ (fix_or_cofix b mfix idx) (fix_or_cofix b mfix' idx).
  Proof using Type.
    destruct b; apply red_fix_body || apply red_cofix_body.
  Qed.

  Lemma ws_cumul_pb_fix_one_body {b Γ mfix mfix' idx} :
    is_closed_context Γ
    is_open_mfix Γ mfix
    is_open_mfix Γ mfix'
    OnOne2 (fun u v
      dtype u = dtype v ×
      Σ ;;; Γ ,,, fix_context mfix dbody u = dbody v ×
      (rarg u = rarg v) ×
      (eq_binder_annot (dname u) (dname v))
    ) mfix mfix'
    Σ ;;; Γ fix_or_cofix b mfix idx = fix_or_cofix b mfix' idx.
  Proof using wfΣ.
    intros onΓ onmfix onmfix' h.
    assert (eq_context_upto_names (fix_context mfix) (fix_context mfix')).
    { clear -h.
      unfold fix_context, mapi.
      generalize 0 at 2 4.
      induction h; intros n.
      + destruct p as [hty [_ [_ eqna]]].
        cbn.
        eapply All2_app; [eapply All2_refl; reflexivity|].
        constructor; cbn; [|constructor].
        constructor; auto. f_equal. auto.
      + cbn.
        eapply All2_app; eauto.
        constructor; auto. constructor; auto. }
    apply OnOne2_split in h
      as [[na ty bo ra] [[na' ty' bo' ra'] [l1 [l2 [[? [h [? ?]]] [? ?]]]]]].
    simpl in ×. subst ty' ra'.
    eapply ws_cumul_pb_red in h as [v [v' [hbo hbo' hcomp]]].
    set (declv := {| dname := na; dtype := ty; dbody := v; rarg := ra |}).
    set (declv' := {| dname := na'; dtype := ty; dbody := v'; rarg := ra |}).
    eapply ws_cumul_pb_red.
     (fix_or_cofix b (l1 ++ declv :: l2) idx), (fix_or_cofix b (l1 ++ declv' :: l2) idx).
    repeat split; auto; rewrite ?is_open_fix_or_cofix //.
    { destruct b; [eapply red_fix_body | eapply red_cofix_body]; rewrite H;
      eapply All2_app.
      all:try eapply All2_refl; intuition auto.
      all:constructor; [|eapply All2_refl; intuition auto].
      all:cbn; intuition auto; rewrite -H //; tas.
      - apply hbo.
      - apply hbo. }
    { eapply red_fix_or_cofix_body. rewrite H0.
      eapply All2_app; try reflexivity.
      { eapply All2_refl; intuition auto. }
      constructor.
      - cbn. intuition auto.
        rewrite -H0.
        eapply red_eq_context_upto_names; tea.
        2:exact hbo'.
        eapply All2_app; auto.
        eapply All2_refl; reflexivity.
      - eapply All2_refl. intros.
        intuition auto. }
    { cbn. apply eq_term_fix_or_cofix. eapply All2_app.
      × eapply All2_refl; intuition auto; reflexivity.
      × constructor; intuition auto; try reflexivity.
        eapply All2_refl; intuition auto; reflexivity. }
  Qed.

  Lemma is_open_fix_onone2 {Γ Δ mfix mfix'} :
    OnOne2
      (fun u v : def term
       (dtype u = dtype v) ×
       (Σ ;;; Γ,,, Δ dbody u = dbody v
        × rarg u = rarg v × eq_binder_annot (dname u) (dname v))) mfix' mfix
    #|Δ| = #|mfix|
    is_open_mfix Γ mfix
    is_open_mfix Γ mfix'.
  Proof using wfΣ.
    cbn.
    intros a hlen hmfix.
    rewrite (OnOne2_length a).
    eapply OnOne2_split in a as [? [? [? [? []]]]].
    destruct a. subst.
    red; rewrite -hmfix.
    rewrite !forallb_app /=. bool_congr. f_equal.
    destruct p. rewrite /test_def /on_free_vars_decl /test_decl /=.
    rewrite e. f_equal.
    destruct p as [e0 w]. apply ws_cumul_pb_is_open_term in e0.
    move/and3P: e0 ⇒ [].
    now rewrite !app_length hlen !app_length /= shiftnP_add_ → →.
  Qed.

  Lemma ws_cumul_pb_fix_bodies {b Γ mfix mfix' idx} :
    is_closed_context Γ
    is_open_mfix Γ mfix
    is_open_mfix Γ mfix'
    All2 (fun u v
        dtype u = dtype v ×
        Σ ;;; Γ ,,, fix_context mfix dbody u = dbody v ×
        (rarg u = rarg v) ×
        (eq_binder_annot (dname u) (dname v)))
      mfix mfix'
    Σ ;;; Γ fix_or_cofix b mfix idx = fix_or_cofix b mfix' idx.
  Proof using wfΣ.
    intros onΓ onm onm' h.
    assert (thm :
      Σ ;;; Γ fix_or_cofix b mfix idx = fix_or_cofix b mfix' idx ×
      #|mfix| = #|mfix'| ×
      eq_context_upto Σ eq eq (Γ ,,, fix_context mfix) (Γ ,,, fix_context mfix')
    ).
    { eapply (All2_many_OnOne2_pres _ (fun xTrue)) in h.
      2:intuition.
      induction h.
      - split; try reflexivity.
        + constructor ⇒ //; rewrite ?is_open_fix_or_cofix //.
          cbn; reflexivity.
        + split; reflexivity.
      - destruct r as [hl [r _]].
        assert (is_open_mfix Γ y).
        { eapply (is_open_fix_onone2) in r; intuition auto.
          now rewrite fix_context_length -(OnOne2_length r) -(rtrans_clos_length h). }
        destruct (IHh H) as [? []].
        split.
        + etransitivity.
          × eassumption.
          × apply ws_cumul_pb_fix_one_body; tea; eauto with fvs.
            eapply OnOne2_impl. 1: eassumption.
            intros [na ty bo ra] [na' ty' bo' ra'] [? [hh ?]].
            simpl in ×. intuition eauto.
            eapply ws_cumul_pb_eq_context_upto. 3: eassumption.
            1:eapply eq_context_impl. 4: eassumption.
            all:tc.
            rewrite on_free_vars_ctx_app onΓ /=.
            apply on_free_vars_fix_context. solve_all.
        + split; [lia|].
          etransitivity.
          × eassumption.
          × apply OnOne2_split in r
              as [[na ty bo ra] [[na' ty' bo' ra'] [l1 [l2 [[? [? [? ?]]] [? ?]]]]]].
            simpl in ×. subst.
            rewrite 2!fix_context_fix_context_alt.
            rewrite 2!map_app. simpl.
            unfold def_sig at 2 5. simpl.
            eapply eq_context_upto_cat.
            -- eapply eq_context_upto_refl; auto.
            -- eapply eq_context_upto_rev'.
               rewrite 2!mapi_app. cbn.
               eapply eq_context_upto_cat.
               ++ constructor; tas; revgoals.
                  ** constructor; tas. eapply eq_term_upto_univ_refl. all: auto.
                  ** eapply eq_context_upto_refl; auto.
               ++ eapply eq_context_upto_refl; auto.
    }
    apply thm.
  Qed.

  Lemma ws_cumul_pb_fix_or_cofix {b Γ mfix mfix' idx} :
    is_closed_context Γ
    All2 (fun u v
      Σ;;; Γ dtype u = dtype v ×
      Σ;;; Γ ,,, fix_context mfix dbody u = dbody v ×
      (rarg u = rarg v) ×
      (eq_binder_annot (dname u) (dname v)))
      mfix mfix'
    Σ ;;; Γ fix_or_cofix b mfix idx = fix_or_cofix b mfix' idx.
  Proof using wfΣ.
    intros onΓ h.
    assert (is_open_mfix Γ mfix is_open_mfix Γ mfix') as [opl opr].
    { cbn. rewrite -(All2_length h). solve_all.
      - move: a a0 ⇒ /ws_cumul_pb_is_open_term /and3P[] _ onty onty'.
        move/ws_cumul_pb_is_open_term ⇒ /and3P[] _.
        rewrite !app_length !fix_context_lengthonbody onbody'.
        rewrite /test_def /= onty /= shiftnP_add //.
      - move: a a0 ⇒ /ws_cumul_pb_is_open_term/and3P[] _ onty onty'.
        move/ws_cumul_pb_is_open_term ⇒ /and3P[] _.
        rewrite !app_length !fix_context_lengthonbody onbody'.
        rewrite /test_def /= onty' /= shiftnP_add //. }
    assert (h' : mfix'',
      All2 (fun u v
        Σ;;; Γ dtype u = dtype v ×
        dbody u = dbody v ×
        rarg u = rarg v ×
        (eq_binder_annot (dname u) (dname v))
      ) mfix'' mfix' ×
      All2 (fun u v
        dtype u = dtype v ×
        Σ;;; Γ ,,, fix_context mfix dbody u = dbody v ×
        rarg u = rarg v ×
        (eq_binder_annot (dname u) (dname v))
      ) mfix mfix''
    ).
    { set (P1 := fun u vΣ ;;; Γ u = v).
      set (P2 := fun u vΣ ;;; Γ ,,, fix_context mfix u = v).
      change (
        All2 (fun u v
          P1 u.(dtype) v.(dtype) ×
          P2 u.(dbody) v.(dbody) ×
          (rarg u = rarg v) ×
          (eq_binder_annot (dname u) (dname v))
        ) mfix mfix'
      ) in h.
      change (
         mfix'',
          All2 (fun u v
            P1 u.(dtype) v.(dtype) × dbody u = dbody v × (rarg u = rarg v) ×
            (eq_binder_annot (dname u) (dname v))
          ) mfix'' mfix' ×
          All2 (fun u v
            dtype u = dtype v × P2 u.(dbody) v.(dbody) × rarg u = rarg v ×
            (eq_binder_annot (dname u) (dname v))
          ) mfix mfix''
      ).
      clearbody P1 P2. clear opl opr.
      induction h.
      - []. repeat split. all: constructor.
      - destruct IHh as [l'' [h1 h2]].
        eexists (mkdef _ (dname x) _ _ _ :: l''). repeat split.
        + constructor. 2: assumption.
          simpl. intuition eauto.
        + constructor. 2: assumption.
          intuition eauto.
    }
    destruct h' as [mfix'' [h1 h2]].
    assert (is_open_mfix Γ mfix'').
    { cbn in opl. eapply forallb_All in opl.
      eapply All2_All_mix_left in h2; tea.
      cbn. rewrite -(All2_length h2). solve_all.
      move: a ⇒ /andP[].
      move: a2 ⇒ /ws_cumul_pb_is_open_term/and3P[] _.
      rewrite !app_length !fix_context_lengthonbody onbody'.
      rewrite /test_def /= a1 ⇒ → /= _.
      rewrite shiftnP_add //. }
    etransitivity.
    - eapply ws_cumul_pb_fix_bodies. 4:tea. all:assumption.
    - eapply ws_cumul_pb_fix_types. all: assumption.
  Qed.

  Lemma ws_cumul_pb_Fix {Γ mfix mfix' idx} :
    is_closed_context Γ
    All2 (fun u v
      Σ;;; Γ dtype u = dtype v ×
      Σ;;; Γ ,,, fix_context mfix dbody u = dbody v ×
      (rarg u = rarg v) ×
      (eq_binder_annot (dname u) (dname v)))
      mfix mfix'
    Σ ;;; Γ tFix mfix idx = tFix mfix' idx.
  Proof using wfΣ. eapply (ws_cumul_pb_fix_or_cofix (b:=true)). Qed.

  Lemma ws_cumul_pb_CoFix {Γ mfix mfix' idx} :
    is_closed_context Γ
    All2 (fun u v
      Σ;;; Γ dtype u = dtype v ×
      Σ;;; Γ ,,, fix_context mfix dbody u = dbody v ×
      (rarg u = rarg v) ×
      (eq_binder_annot (dname u) (dname v)))
      mfix mfix'
    Σ ;;; Γ tCoFix mfix idx = tCoFix mfix' idx.
  Proof using wfΣ. eapply (ws_cumul_pb_fix_or_cofix (b:=false)). Qed.

  Lemma ws_cumul_pb_eq_le_gen {pb Γ T U} :
    Σ ;;; Γ T = U
    Σ ;;; Γ T ≤[pb] U.
  Proof using Type.
    destruct pb ⇒ //.
    eapply ws_cumul_pb_eq_le.
  Qed.

  Lemma ws_cumul_pb_Lambda_l {Γ na A b na' A' pb} :
    eq_binder_annot na na'
    is_open_term (Γ ,, vass na A) b
    Σ ;;; Γ A = A'
    Σ ;;; Γ tLambda na A b ≤[pb] tLambda na' A' b.
  Proof using wfΣ.
    intros hna hb h.
    eapply ws_cumul_pb_eq_le_gen.
    eapply into_ws_cumul_pb.
    { clear -h hna; induction h.
      - constructor; constructor; auto; reflexivity.
      - eapply cumul_red_l; tea; pcuic.
      - eapply cumul_red_r; tea; pcuic. }
    { eauto with fvs. }
    all:rewrite on_fvs_lambda; eauto with fvs.
  Qed.

  Lemma ws_cumul_pb_Lambda_r {pb Γ na A b b'} :
    Σ ;;; Γ,, vass na A b ≤[pb] b'
    Σ ;;; Γ tLambda na A b ≤[pb] tLambda na A b'.
  Proof using wfΣ.
    intros h.
    generalize (ws_cumul_pb_is_closed_context h).
    rewrite on_free_vars_ctx_snoc /on_free_vars_decl /test_decl ⇒ /andP[] onΓ /= onA.
    eapply into_ws_cumul_pb ⇒ //.
    { induction h.
      - destruct pb; now repeat constructor.
      - destruct pb;
         eapply cumul_red_l ; try eassumption; try econstructor; assumption.
      - destruct pb;
         eapply cumul_red_r ; pcuic. }
    all:rewrite on_fvs_lambda onA /=; eauto with fvs.
  Qed.

  Lemma ws_cumul_pb_LetIn_bo {pb Γ na ty t u u'} :
    Σ ;;; Γ ,, vdef na ty t u ≤[pb] u'
    Σ ;;; Γ tLetIn na ty t u ≤[pb] tLetIn na ty t u'.
  Proof using wfΣ.
    intros h.
    generalize (ws_cumul_pb_is_open_term h).
    rewrite on_free_vars_ctx_snoc /= ⇒ /and3P[]/andP[] onΓ.
    rewrite /on_free_vars_decl /test_decl ⇒ /andP[] /= onty ont onu onu'.
    eapply into_ws_cumul_pb ⇒ //.
    { clear -h. induction h.
      - destruct pb;
        eapply cumul_refl; constructor.
        all: try reflexivity; auto.
      - destruct pb;
        eapply cumul_red_l; tea; pcuic.
      - destruct pb;
        eapply cumul_red_r ; pcuic. }
    { rewrite on_fvs_letin onty ont //. }
    { rewrite on_fvs_letin onty ont //. }
  Qed.

  Lemma ws_cumul_pb_it_mkLambda_or_LetIn_codom {Δ Γ u v pb} :
      Σ ;;; (Δ ,,, Γ) u ≤[pb] v
      Σ ;;; Δ it_mkLambda_or_LetIn Γ u ≤[pb] it_mkLambda_or_LetIn Γ v.
  Proof using wfΣ.
    intros h. revert Δ u v h.
    induction Γ as [| [na [b|] A] Γ ih ] ; intros Δ u v h.
    - assumption.
    - simpl. cbn. eapply ih.
      eapply ws_cumul_pb_LetIn_bo. assumption.
    - simpl. cbn. eapply ih.
      eapply ws_cumul_pb_Lambda_r. assumption.
  Qed.

  Lemma ws_cumul_pb_it_mkProd_or_LetIn_codom {Δ Γ B B' pb} :
      Σ ;;; (Δ ,,, Γ) B ≤[pb] B'
      Σ ;;; Δ it_mkProd_or_LetIn Γ B ≤[pb] it_mkProd_or_LetIn Γ B'.
  Proof using wfΣ.
    intros h.
    induction Γ as [| [na [b|] A] Γ ih ] in Δ, B, B', h |- ×.
    - assumption.
    - simpl. cbn. eapply ih.
      eapply ws_cumul_pb_LetIn_bo. assumption.
    - simpl. cbn. eapply ih.
      eapply ws_cumul_pb_Prod; try reflexivity; tas.
      move/ws_cumul_pb_is_closed_context: h.
      rewrite /= on_free_vars_ctx_snoc /on_free_vars_decl /test_decl /= ⇒ /andP[] onΓΔ ont.
      apply ws_cumul_pb_refl ⇒ //.
  Qed.

  Lemma ws_cumul_pb_mkApps_weak :
     Γ u1 u2 l,
      forallb (is_open_term Γ) l
      Σ ;;; Γ u1 = u2
      Σ ;;; Γ mkApps u1 l = mkApps u2 l.
  Proof using wfΣ.
    intros Γ u1 u2 l.
    induction l in u1, u2 |- *; cbn. 1: trivial.
    move⇒ /andP[] ona onl.
    intros X. apply IHl ⇒ //. apply ws_cumul_pb_App_l ⇒ //.
  Qed.

  Lemma ws_cumul_pb_Lambda {pb Γ na1 na2 A1 A2 t1 t2} :
    eq_binder_annot na1 na2
    Σ ;;; Γ A1 = A2
    Σ ;;; Γ ,, vass na1 A1 t1 ≤[pb] t2
    Σ ;;; Γ tLambda na1 A1 t1 ≤[pb] tLambda na2 A2 t2.
  Proof using wfΣ.
    intros eqna X.
    etransitivity.
    - eapply ws_cumul_pb_Lambda_r; tea.
    - destruct pb; revgoals.
      + eapply ws_cumul_pb_eq_le, ws_cumul_pb_Lambda_l ⇒ //. eauto with fvs.
      + eapply ws_cumul_pb_Lambda_l; tea; eauto with fvs.
  Qed.

  Lemma conv_cum_Lambda leq Γ na1 na2 A1 A2 t1 t2 :
    eq_binder_annot na1 na2
    Σ ;;; Γ A1 = A2
    sq_ws_cumul_pb leq Σ (Γ ,, vass na1 A1) t1 t2
    sq_ws_cumul_pb leq Σ Γ (tLambda na1 A1 t1) (tLambda na2 A2 t2).
  Proof using wfΣ.
    intros eqna X []; sq. now apply ws_cumul_pb_Lambda.
  Qed.

  Lemma ws_cumul_pb_LetIn_tm Γ na na' ty t t' u :
    eq_binder_annot na na'
    is_open_term Γ ty
    is_open_term (Γ ,, vdef na t ty) u
    Σ ;;; Γ t = t'
    Σ ;;; Γ tLetIn na t ty u = tLetIn na' t' ty u.
  Proof using wfΣ.
    intros hna onty onu ont.
    eapply into_ws_cumul_pb.
    { clear onu. induction ont.
      - constructor 1. constructor; try reflexivity;
        assumption.
      - econstructor 2; tea. now constructor.
      - econstructor 3; tea. now constructor. }
    { eauto with fvs. }
    all:rewrite on_fvs_letin onty; eauto with fvs.
  Qed.

  Lemma ws_cumul_pb_LetIn_ty {Γ na na' ty ty' t u} :
    eq_binder_annot na na'
    is_open_term Γ t
    is_open_term (Γ ,, vdef na t ty) u
    Σ ;;; Γ ty = ty'
    Σ ;;; Γ tLetIn na t ty u = tLetIn na' t ty' u.
  Proof using wfΣ.
    intros hna ont onu onty.
    eapply into_ws_cumul_pb.
    { clear onu. induction onty.
      - constructor 1. constructor; try reflexivity;
        assumption.
      - econstructor 2; tea. now constructor.
      - econstructor 3; tea. now constructor. }
    { eauto with fvs. }
    all:rewrite on_fvs_letin ont onu andb_true_r; eauto with fvs.
  Qed.

  Lemma ws_cumul_pb_LetIn {pb Γ na1 na2 t1 t2 A1 A2 u1 u2} :
    eq_binder_annot na1 na2
    Σ;;; Γ t1 = t2
    Σ;;; Γ A1 = A2
    Σ ;;; Γ ,, vdef na1 t1 A1 u1 ≤[pb] u2
    Σ ;;; Γ tLetIn na1 t1 A1 u1 ≤[pb] tLetIn na2 t2 A2 u2.
  Proof using wfΣ.
    intros hna ont ona onu.
    etransitivity.
    { eapply ws_cumul_pb_LetIn_bo; tea. }
    eapply ws_cumul_pb_eq_le_gen.
    etransitivity.
    { eapply ws_cumul_pb_LetIn_ty; tea; eauto with fvs. }
    eapply ws_cumul_pb_LetIn_tm; tea; eauto with fvs.
    now move/ws_cumul_pb_is_open_term_right: onu.
  Qed.

  Lemma ws_cumul_pb_it_mkLambda_or_LetIn {pb Γ Δ1 Δ2 t1 t2} :
    Σ Γ ,,, Δ1 = Γ ,,, Δ2
    Σ ;;; Γ ,,, Δ1 t1 ≤[pb] t2
    Σ ;;; Γ it_mkLambda_or_LetIn Δ1 t1 ≤[pb] it_mkLambda_or_LetIn Δ2 t2.
  Proof using wfΣ.
    induction Δ1 in Δ2, t1, t2 |- *; intros X Y.
    - apply All2_fold_length in X.
      destruct Δ2; cbn in *; [trivial|].
      rewrite app_length in X; lia.
    - apply All2_fold_length in X as X'.
      destruct Δ2 as [|c Δ2]; simpl in *; [rewrite app_length in X'; lia|].
      dependent destruction X.
      + eapply IHΔ1; tas; cbn.
        depelim w.
        × eapply ws_cumul_pb_Lambda; simpl; tea.
        × eapply ws_cumul_pb_LetIn; simpl; tea.
  Qed.

  Lemma invert_red_lambda Γ na A1 b1 T :
    Σ ;;; Γ (tLambda na A1 b1) T
     A2 b2, T = tLambda na A2 b2,
        Σ ;;; Γ A1 A2 & Σ ;;; (Γ ,, vass na A1) b1 b2].
  Proof using wfΣ.
    intros [onΓ onl ont].
    rewrite on_fvs_lambda in onl.
    move: onl ⇒ /=/andP [] onA1 onb1.
    eapply clos_rt_rt1n_iff in ont. depind ont.
    - eexists _, _. split ⇒ //.
      eapply closed_red_refl; eauto with fvs.
    - depelim r; solve_discr; specialize (IHont _ _ _ _ onΓ eq_refl byfvs).
      + forward IHont by tas.
        destruct IHont as [A2 [B2 [-> [? ?]]]].
        eexists _, _; split ⇒ //.
        1:{ split; tas. eapply red_step with M' ⇒ //. }
        eapply red_red_ctx_inv'; eauto.
        constructor; auto.
        × now eapply closed_red_ctx_refl.
        × constructor; auto.
          split; tas; pcuic.
      + forward IHont.
        { eapply red1_on_free_vars; tea.
          rewrite (@on_free_vars_ctx_on_ctx_free_vars _ (Γ ,, vass na A1)).
          eauto with fvs. }
          destruct IHont as [A2 [B2 [-> [? ?]]]].
          eexists _, _; split ⇒ //.
          split; eauto with fvs. eapply red_step with M' ⇒ //.
          apply c.
  Qed.

  Lemma ws_cumul_pb_Lambda_inv :
     pb Γ na1 na2 A1 A2 b1 b2,
      Σ ;;; Γ tLambda na1 A1 b1 ≤[pb] tLambda na2 A2 b2
       eq_binder_annot na1 na2, Σ ;;; Γ A1 = A2 & Σ ;;; Γ ,, vass na1 A1 b1 ≤[pb] b2].
  Proof using wfΣ.
    intros ×.
    move/ws_cumul_pb_red; intros (v & v' & [redv redv' eq]).
    eapply invert_red_lambda in redv as (A1' & b1' & [-> rA1 rb1]).
    eapply invert_red_lambda in redv' as (v0 & v0' & [redv0 redv0' eq0]).
    subst v'.
    destruct pb; depelim eq.
    { assert (Σ ;;; Γ A1 = A2).
      - eapply ws_cumul_pb_red.
         A1', v0; split=>//.
      - split ⇒ //. transitivity b1'; pcuic.
        eapply ws_cumul_pb_ws_cumul_ctx; revgoals.
        { transitivity v0'; tea. 2:eapply red_ws_cumul_pb_inv; tea.
          constructor; tea. 1,3:eauto with fvs.
          now generalize (closed_red_open_right rb1). }
        constructor.
        { eapply ws_cumul_ctx_pb_refl; eauto with fvs. }
        constructor; eauto. }
    { assert (Σ ;;; Γ A1 = A2).
      - eapply ws_cumul_pb_red.
         A1', v0; split; auto.
      - split=>//. transitivity b1'; pcuic.
        eapply ws_cumul_pb_ws_cumul_ctx; revgoals.
        { transitivity v0'; tea. 2:eapply red_ws_cumul_pb_inv; tea.
          constructor; tea. 1,3:eauto with fvs.
          now generalize (closed_red_open_right rb1). }
        constructor.
        { eapply ws_cumul_ctx_pb_refl; eauto with fvs. }
        constructor; eauto. }
  Qed.

  Lemma Lambda_conv_cum_inv :
     leq Γ na1 na2 A1 A2 b1 b2,
      sq_ws_cumul_pb leq Σ Γ (tLambda na1 A1 b1) (tLambda na2 A2 b2)
      eq_binder_annot na1 na2 Σ ;;; Γ A1 = A2 sq_ws_cumul_pb leq Σ (Γ ,, vass na1 A1) b1 b2.
  Proof using wfΣ.
    intros × []. eapply ws_cumul_pb_Lambda_inv in X as [].
    intuition auto. all:sq; auto.
  Qed.

End ConvRedConv.


Section ConvSubst.
  Context {cf : checker_flags} {Σ : global_env_ext} {wfΣ : wf Σ}.

  Lemma subslet_open {Γ s Γ'} : subslet Σ Γ s Γ'
    forallb (is_open_term Γ) s.
  Proof using wfΣ.
    induction 1; simpl; auto.
    - apply subject_closed in t0.
      rewrite (closedn_on_free_vars t0) //.
    - eapply subject_closed in t0.
      rewrite (closedn_on_free_vars t0) //.
  Qed.
  Hint Resolve subslet_open : fvs.

  Lemma untyped_closed_red_subst {Γ Δ Γ' s M N} :
    untyped_subslet Γ s Δ
    forallb (is_open_term Γ) s
    Σ ;;; Γ ,,, Δ ,,, Γ' M N
    Σ ;;; Γ ,,, subst_context s 0 Γ' subst s #|Γ'| M subst s #|Γ'| N.
  Proof using wfΣ.
    intros Hs Hs' H. split.
    - eapply is_closed_subst_context; eauto with fvs pcuic.
      eapply (untyped_subslet_length Hs).
    - eapply is_open_term_subst; tea; eauto with fvs pcuic.
      eapply (untyped_subslet_length Hs).
    - eapply substitution_untyped_red; tea; eauto with fvs.
  Qed.

  Lemma closed_red_subst {Γ Δ Γ' s M N} :
    subslet Σ Γ s Δ
    Σ ;;; Γ ,,, Δ ,,, Γ' M N
    Σ ;;; Γ ,,, subst_context s 0 Γ' subst s #|Γ'| M subst s #|Γ'| N.
  Proof using wfΣ.
    intros Hs H. split.
    - eapply is_closed_subst_context; eauto with fvs pcuic.
      eapply (subslet_length Hs).
    - eapply is_open_term_subst; tea; eauto with fvs pcuic.
      eapply (subslet_length Hs).
    - eapply substitution_untyped_red; tea; eauto with fvs.
      now eapply subslet_untyped_subslet.
  Qed.

  Lemma untyped_substitution_ws_cumul_pb {pb Γ Γ' Γ'' s M N} :
    untyped_subslet Γ s Γ'
    forallb (is_open_term Γ) s
    Σ ;;; Γ ,,, Γ' ,,, Γ'' M ≤[pb] N
    Σ ;;; Γ ,,, subst_context s 0 Γ'' subst s #|Γ''| M ≤[pb] subst s #|Γ''| N.
  Proof using wfΣ.
    intros Hs Hs'. induction 1.
    - cbn. constructor; eauto with fvs.
      { eapply is_closed_subst_context; tea; eauto with fvs.
        now apply (untyped_subslet_length Hs). }
      { eapply is_open_term_subst; tea; eauto with fvs.
        now eapply (untyped_subslet_length Hs). }
      { eapply is_open_term_subst; tea; eauto with fvs.
        now apply (untyped_subslet_length Hs). }
      now apply subst_compare_term.
    - eapply red_ws_cumul_pb_left; tea.
      eapply untyped_closed_red_subst; tea.
      constructor; eauto.
    - eapply red_ws_cumul_pb_right; tea.
      eapply untyped_closed_red_subst; tea.
      constructor; eauto.
  Qed.

  Lemma substitution_ws_cumul_pb {pb Γ Γ' Γ'' s M N} :
    subslet Σ Γ s Γ'
    Σ ;;; Γ ,,, Γ' ,,, Γ'' M ≤[pb] N
    Σ ;;; Γ ,,, subst_context s 0 Γ'' subst s #|Γ''| M ≤[pb] subst s #|Γ''| N.
  Proof using wfΣ.
    intros Hs. induction 1.
    - cbn. constructor; eauto with fvs.
      { eapply is_closed_subst_context; tea; eauto with fvs.
        now apply (subslet_length Hs). }
      { eapply is_open_term_subst; tea; eauto with fvs.
        now eapply (subslet_length Hs). }
      { eapply is_open_term_subst; tea; eauto with fvs.
        now apply (subslet_length Hs). }
      now apply subst_compare_term.
    - eapply red_ws_cumul_pb_left; tea.
      eapply closed_red_subst; tea.
      constructor; eauto.
    - eapply red_ws_cumul_pb_right; tea.
      eapply closed_red_subst; tea.
      constructor; eauto.
  Qed.

  Lemma substitution0_ws_cumul_pb {pb Γ na T t M N} :
    Σ ;;; Γ |- t : T
    Σ ;;; Γ ,, vass na T M ≤[pb] N
    Σ ;;; Γ M{0 := t} ≤[pb] N{0 := t}.
  Proof using wfΣ.
    intros.
    eapply (substitution_ws_cumul_pb (Γ' := [vass na T]) (Γ'' := [])); cbn; tea.
    now eapply subslet_ass_tip.
  Qed.

  Derive Signature for untyped_subslet.

  Lemma ws_cumul_pb_substs_red {Γ Δ s s'} :
    ws_cumul_pb_terms Σ Γ s s'
    untyped_subslet Γ s Δ
     s0 s'0, All2 (closed_red Σ Γ) s s0, All2 (closed_red Σ Γ) s' s'0 & All2 (eq_term Σ Σ) s0 s'0].
  Proof using wfΣ.
    moveeqsub subs.
    induction eqsub in Δ, subs |- ×.
    × depelim subs. [], []; split; auto.
    × depelim subs.
    - specialize (IHeqsub _ subs) as [s0 [s'0 [redl redr eqs0]]].
      eapply ws_cumul_pb_red in r as [v [v' [redv redv' eqvv']]].
       (v :: s0), (v' :: s'0). repeat split; constructor; auto.
    - specialize (IHeqsub _ subs) as [s0 [s'0 [redl redr eqs0]]].
      eapply ws_cumul_pb_red in r as [v [v' [redv redv' eqvv']]].
       (v :: s0), (v' :: s'0). repeat split; constructor; auto.
  Qed.

  Lemma All2_fold_fold_context_k P (f g : nat term term) ctx ctx' :
    All2_fold (fun Γ Γ' d d'P (fold_context_k f Γ) (fold_context_k g Γ')
    (map_decl (f #|Γ|) d) (map_decl (g #|Γ'|) d')) ctx ctx'
    All2_fold P (fold_context_k f ctx) (fold_context_k g ctx').
  Proof using Type.
    intros a. rewrite - !mapi_context_fold.
    eapply All2_fold_mapi.
    eapply All2_fold_impl_ind; tea.
    intros par par' x y H IH; cbn.
    rewrite !mapi_context_fold.
    now rewrite -(length_of H).
  Qed.

  Lemma All_decls_alpha_pb_impl le P Q d d' :
    All_decls_alpha_pb le P d d'
    ( le x y, P le x y Q le x y)
    All_decls_alpha_pb le Q d d'.
  Proof using Type.
    intros [] H; constructor; auto.
  Qed.

  Lemma All_decls_alpha_pb_map le P f g d d' :
    All_decls_alpha_pb le (fun le x yP le (f x) (g y)) d d'
    All_decls_alpha_pb le P (map_decl f d) (map_decl g d').
  Proof using Type.
    intros []; constructor; cbn; auto.
  Qed.

  Lemma test_decl_conv_decls_map {Γ Γ' : context} {p f g} {d : context_decl} :
    test_decl p d
    ( x, p x convAlgo Σ Γ (f x) (g x))
    conv_decls cumulAlgo_gen Σ Γ Γ' (map_decl f d) (map_decl g d).
  Proof using Type.
    intros ht hxy.
    destruct d as [na [b|] ty]; cbn; constructor; try red; eauto.
    - move/andP: ht ⇒ /= [] pb pty; eauto.
    - move/andP: ht ⇒ /= [] pb pty; eauto.
  Qed.

  Lemma substitution_ws_cumul_ctx_pb_red_subst {Γ Δ Γ' s s'} :
    is_closed_context (Γ ,,, Δ ,,, Γ')
    All2 (closed_red Σ Γ) s s'
    untyped_subslet Γ s Δ
    Σ Γ ,,, subst_context s 0 Γ' = Γ ,,, subst_context s' 0 Γ'.
  Proof using wfΣ.
    intros.
    eapply into_ws_cumul_ctx_pb.
    { eapply is_closed_subst_context; tea; solve_all; eauto with fvs.
      apply (untyped_subslet_length X0). }
    { eapply is_closed_subst_context; tea; solve_all; eauto with fvs.
      rewrite -(All2_length X). apply (untyped_subslet_length X0). }
    eapply All2_fold_app; len ⇒ //; try reflexivity.
    eapply All2_fold_fold_context_k.
    induction Γ'; constructor; auto.
    { apply IHΓ'. move: H; rewrite /= on_free_vars_ctx_snoc ⇒ /andP[] //. }
    move: H; rewrite /= on_free_vars_ctx_snoc ⇒ /andP[] // iscl wsdecl.
    eapply test_decl_conv_decls_map; tea.
    intros x hx.
    eapply PCUICCumulativity.red_conv.
    rewrite - !/(subst_context _ _ _) Nat.add_0_r.
    eapply red_red; tea.
    { erewrite on_free_vars_ctx_on_ctx_free_vars; tea. }
    { solve_all; pcuic. exact X1. }
    { solve_all. rewrite !app_length Nat.add_assoc -shiftnP_add addnP_shiftnP.
      eauto with fvs. }
  Qed.

  Lemma subst_context_app0 s Γ Γ' :
    subst_context s 0 Γ ,,, subst_context s #|Γ| Γ' =
    subst_context s 0 (Γ ,,, Γ').
  Proof using Type.
    now rewrite -(Nat.add_0_r #|Γ|) subst_context_app.
  Qed.

  Lemma eq_context_upto_ws_cumul_ctx_pb {pb Γ Γ'} :
    is_closed_context Γ
    is_closed_context Γ'
    eq_context_upto Σ (eq_universe Σ) (compare_universe pb Σ) Γ Γ'
    ws_cumul_ctx_pb pb Σ Γ Γ'.
  Proof using wfΣ.
    intros cl cl' eq.
    apply into_ws_cumul_ctx_pb; auto.
    destruct pb; revgoals.
    { now eapply eq_context_upto_univ_cumul_context. }
    { now eapply eq_context_upto_univ_conv_context. }
  Qed.

  Lemma substitution_ws_cumul_ctx_pb {Γ Δ Δ' Γ' s s'} :
    untyped_subslet Γ s Δ
    untyped_subslet Γ s' Δ'
    ws_cumul_pb_terms Σ Γ s s'
    is_closed_context (Γ ,,, Δ ,,, Γ')
    is_closed_context (Γ ,,, Δ' ,,, Γ')
    Σ Γ ,,, subst_context s 0 Γ' = Γ ,,, subst_context s' 0 Γ'.
  Proof using wfΣ.
    movesubs subs' eqsub cl cl'.
    destruct (ws_cumul_pb_substs_red eqsub subs) as (s0 & s'0 & [rs' rs'0 eqs]).
    transitivity (Γ ,,, subst_context s0 0 Γ').
    { eapply substitution_ws_cumul_ctx_pb_red_subst; revgoals; tea. }
    symmetry. transitivity (Γ ,,, subst_context s'0 0 Γ').
    { eapply substitution_ws_cumul_ctx_pb_red_subst; revgoals; tea. }
    eapply eq_context_upto_ws_cumul_ctx_pb.
    { clear eqs; eapply is_closed_subst_context; tea; solve_all; eauto with fvs.
      rewrite -(All2_length rs'0). apply (untyped_subslet_length subs'). }
    { clear eqs; eapply is_closed_subst_context; tea; solve_all; eauto with fvs.
      rewrite -(All2_length rs') (All2_length eqsub). apply (untyped_subslet_length subs'). }
    eapply eq_context_upto_cat; try reflexivity.
    apply eq_context_upto_subst_context; tc; try reflexivity.
    eapply All2_symP; tc. assumption.
  Qed.

  Lemma untyped_substitution_ws_cumul_pb_subst_conv {Γ Δ Δ' Γ' s s' b} :
    ws_cumul_pb_terms Σ Γ s s'
    is_closed_context (Γ ,,, Δ ,,, Γ')
    is_closed_context (Γ ,,, Δ' ,,, Γ')
    untyped_subslet Γ s Δ
    untyped_subslet Γ s' Δ'
    is_open_term (Γ ,,, Δ ,,, Γ') b
    Σ ;;; Γ ,,, subst_context s 0 Γ' subst s #|Γ'| b = subst s' #|Γ'| b.
  Proof using wfΣ.
    moveeqsub cl cl' subs subs' clb.
    assert( s0 s'0, All2 (closed_red Σ Γ) s s0, All2 (closed_red Σ Γ) s' s'0 & All2 (eq_term Σ Σ) s0 s'0])
      as [s0 [s'0 [redl redr eqs]]].
    { apply (ws_cumul_pb_substs_red eqsub subs). }
    etransitivity.
    × apply red_conv. apply (closed_red_red_subst (Δ := Δ) (s' := s0)); tas.
    × symmetry; etransitivity.
    ** eapply ws_cumul_pb_ws_cumul_ctx; revgoals.
      + apply red_conv. eapply (closed_red_red_subst (Δ := Δ') (s' := s'0)); tea.
        rewrite !app_length -(untyped_subslet_length subs') -(All2_length eqsub).
        rewrite (untyped_subslet_length subs) - !app_length //.
      + eapply substitution_ws_cumul_ctx_pb; tea.
    ** assert (All (is_open_term Γ) s0) by (eapply (All2_All_right redl); eauto with fvs).
      assert (All (is_open_term Γ) s'0) by (eapply (All2_All_right redr); eauto with fvs).
      eapply ws_cumul_pb_compare.
      { eapply (is_closed_subst_context _ Δ); tea. 1:solve_all; eauto with fvs.
        apply (untyped_subslet_length subs). }
      { eapply is_open_term_subst_gen. 6:tea. all:tea; solve_all; eauto with fvs.
        1:apply (untyped_subslet_length subs).
        now rewrite (All2_length eqsub) (All2_length redr). }
      { eapply is_open_term_subst_gen. 6:tea. all:tea; solve_all; eauto with fvs.
        1:apply (untyped_subslet_length subs).
        now rewrite (All2_length redl). }
      cbn; symmetry.
      eapply eq_term_upto_univ_substs; tc; try reflexivity.
      solve_all.
  Qed.

  Lemma substitution_ws_cumul_pb_subst_conv {pb Γ Γ0 Γ1 Δ s s' T U} :
    untyped_subslet Γ s Γ0
    untyped_subslet Γ s' Γ1
    ws_cumul_pb_terms Σ Γ s s'
    is_closed_context (Γ ,,, Γ1)
    Σ;;; Γ ,,, Γ0 ,,, Δ T ≤[pb] U
    Σ;;; Γ ,,, subst_context s 0 Δ subst s #|Δ| T ≤[pb] subst s' #|Δ| U.
  Proof using wfΣ.
    movesubss subss' eqsub cl eqty.
    generalize (ws_cumul_pb_is_open_term eqty) ⇒ /and3P[] clctx clT clU.
    assert (#|Γ0| = #|Γ1|).
    { rewrite -(untyped_subslet_length subss) -(untyped_subslet_length subss').
      apply (All2_length eqsub). }
    assert (is_open_term (Γ ,,, Γ1 ,,, Δ) U).
    { move: clU. now rewrite !app_context_length H. }
    assert (is_open_term (Γ ,,, Γ1 ,,, Δ) T).
    { move: clT. now rewrite !app_context_length H. }
    assert (is_closed_context (Γ ,,, Γ1 ,,, Δ)).
    { rewrite on_free_vars_ctx_app cl /=.
      move: clctx. rewrite on_free_vars_ctx_app !app_context_length H ⇒ /andP[] //. }
    etransitivity.
    × eapply untyped_substitution_ws_cumul_pb; tea. fvs.
    × eapply ws_cumul_pb_eq_le_gen.
      eapply (untyped_substitution_ws_cumul_pb_subst_conv (Δ := Γ0) (Δ' := Γ1)); tea; eauto.
  Qed.

  Lemma ws_cumul_pb_elim {pb} {Γ} {x y} :
    ws_cumul_pb pb Σ Γ x y
     is_closed_context Γ, is_open_term Γ x, is_open_term Γ y &
      Σ ;;; Γ |- x <=[pb] y].
  Proof using wfΣ.
    intros ws.
    repeat split; eauto with fvs.
    now eapply ws_cumul_pb_forget in ws.
  Qed.

  Lemma is_closed_context_lift Γ Γ'' Γ' :
    is_closed_context (Γ,,, Γ')
    is_closed_context (Γ,,, Γ'')
    is_closed_context (Γ,,, Γ'',,, lift_context #|Γ''| 0 Γ').
  Proof using Type.
    movecl cl'.
    rewrite on_free_vars_ctx_app cl' /=.
    rewrite on_free_vars_ctx_lift_context0 //.
    rewrite app_length -shiftnP_add addnP_shiftnP //.
    move: cl. rewrite on_free_vars_ctx_app ⇒ /andP[] //.
  Qed.
  Hint Resolve is_closed_context_lift : fvs.

  Lemma is_open_term_lift Γ Γ' Γ'' t :
    is_open_term (Γ ,,, Γ') t
    is_open_term (Γ ,,, Γ'' ,,, lift_context #|Γ''| 0 Γ') (lift #|Γ''| #|Γ'| t).
  Proof using Type.
    intros op.
    eapply on_free_vars_impl.
    2:erewrite on_free_vars_lift; tea.
    intros i.
    rewrite /strengthenP /shiftnP /= !orb_false_r !app_length lift_context_length.
    repeat nat_compare_specs ⇒ //.
  Qed.
  Hint Resolve is_open_term_lift : fvs.

  Lemma weakening_ws_cumul_pb {pb Γ Γ' Γ'' M N} :
    Σ ;;; Γ ,,, Γ' M ≤[pb] N
    is_closed_context (Γ ,,, Γ'')
    Σ ;;; Γ ,,, Γ'' ,,, lift_context #|Γ''| 0 Γ' lift #|Γ''| #|Γ'| M ≤[pb] lift #|Γ''| #|Γ'| N.
  Proof using wfΣ.
    move⇒ /ws_cumul_pb_elim [] iscl onM onN eq onΓ''.
    eapply into_ws_cumul_pb; eauto with fvs.
    destruct pb; revgoals.
    { eapply weakening_cumul in eq; eauto with fvs. }
    { eapply weakening_conv in eq; eauto with fvs. }
  Qed.

  Lemma weakening_ws_cumul_pb_eq {Γ Γ' Γ'' : context} {M N : term} k :
    k = #|Γ''|
    Σ;;; Γ ,,, Γ' M = N
    is_closed_context (Γ ,,, Γ'')
    Σ;;; Γ ,,, Γ'' ,,, lift_context k 0 Γ' lift k #|Γ'| M = lift k #|Γ'| N.
  Proof using wfΣ.
    introsconv; eapply weakening_ws_cumul_pb; auto.
  Qed.

  Lemma weaken_ws_cumul_pb {pb Γ t u} Δ :
    is_closed_context Δ
    Σ ;;; Γ t ≤[pb] u
    Σ ;;; Δ ,,, Γ t ≤[pb] u.
  Proof using wfΣ.
    moveclΔ a.
    epose proof (weakening_ws_cumul_pb (Γ := []) (Γ'' := Δ)).
    rewrite !app_context_nil_l in X.
    specialize (X a clΔ).
    rewrite !lift_closed in X ⇒ //; eauto with fvs.
    rewrite closed_ctx_lift in X.
    1:rewrite is_closed_ctx_closed //; eauto with fvs.
    assumption.
  Qed.

End ConvSubst.

#[global] Hint Rewrite @on_free_vars_subst_instance : fvs.
#[global] Hint Rewrite @on_free_vars_ctx_subst_instance subst_instance_length : fvs.

Lemma subst_instance_ws_cumul_pb {cf : checker_flags} (Σ : global_env_ext) Γ u A B univs pb :
  valid_constraints (global_ext_constraints (Σ.1, univs))
                    (subst_instance_cstrs u Σ)
  Σ ;;; Γ A ≤[pb] B
  (Σ.1,univs) ;;; Γ@[u] A@[u] ≤[pb] B@[u].
Proof.
  intros HH X0. induction X0.
  - econstructor. 1-3:eauto with fvs.
    destruct pb; revgoals.
    × eapply leq_term_subst_instance; tea.
    × eapply eq_term_subst_instance; tea.
  - econstructor 2; revgoals; cycle 1.
    { eapply (red1_subst_instance Σ.1 Γ u t v r). }
    all:eauto with fvs.
  - econstructor 3. 6:eapply red1_subst_instance; cbn; eauto.
    all: eauto with fvs.
Qed.

Definition ws_cumul_ctx_pb_rel {cf} pb Σ Γ Δ Δ' :=
  is_closed_context Γ ×
  All2_fold (fun Γ' _All_decls_alpha_pb pb (fun pb x yΣ ;;; Γ ,,, Γ' x ≤[pb] y)) Δ Δ'.

Lemma ws_cumul_ctx_pb_rel_app {cf} {Σ} {wfΣ : wf Σ} {pb Γ Δ Δ'} :
  ws_cumul_ctx_pb_rel pb Σ Γ Δ Δ' <~>
  ws_cumul_ctx_pb pb Σ (Γ ,,, Δ) (Γ ,,, Δ').
Proof.
  split; intros h.
  + eapply All2_fold_app ⇒ //.
    × destruct h. now apply ws_cumul_ctx_pb_refl.
    × eapply All2_fold_impl; tea. 1:apply h.
      intros ???? []; constructor; auto.
  + eapply All2_fold_app_inv in h as [].
    2:{ move: (length_of h). len; lia. }
    split.
    { now apply ws_cumul_ctx_pb_closed_left in a. }
    eapply All2_fold_impl; tea ⇒ /=.
    intros ???? []; constructor; auto.
Qed.

Lemma subst_instance_ws_cumul_ctx_pb {cf:checker_flags} {Σ : global_env_ext} {wfΣ : wf Σ} {Δ u u'} pb :
  wf_local Σ (subst_instance u Δ)
  R_universe_instance (eq_universe (global_ext_constraints Σ)) u u'
  ws_cumul_ctx_pb pb Σ (subst_instance u Δ) (subst_instance u' Δ).
Proof.
  movewf equ.
  eapply All2_fold_map.
  induction Δ as [|d Δ] in wf |- ×.
  - constructor.
  - simpl. depelim wf.
    × cbn; constructor.
      + apply IHΔ ⇒ //.
      + destruct d as [na [b|] ty]; constructor; cbn in *; auto; try congruence.
        destruct l as [s Hs].
        constructor. 1:eauto with fvs.
        { now eapply subject_closed in Hs; rewrite is_open_term_closed in Hs. }
        { erewrite on_free_vars_subst_instance.
          eapply subject_closed in Hs; rewrite is_open_term_closed in Hs.
          now rewrite on_free_vars_subst_instance in Hs. }
        destruct pb; apply eq_term_upto_univ_subst_instance; try typeclasses eauto; auto.
    × cbn; constructor.
      + apply IHΔ ⇒ //.
      + destruct d as [na [b'|] ty]; constructor; cbn in *; auto; try congruence; noconf H.
        { destruct l as [s Hs].
          constructor. 1:eauto with fvs.
          { now eapply subject_closed in l0; rewrite is_open_term_closed in l0. }
          { erewrite on_free_vars_subst_instance.
            eapply subject_closed in l0; rewrite is_open_term_closed in l0.
            now rewrite on_free_vars_subst_instance in l0. }
          apply eq_term_upto_univ_subst_instance; try typeclasses eauto. auto. }
        { destruct l as [s Hs].
          constructor. 1:eauto with fvs.
          { now eapply subject_closed in Hs; rewrite is_open_term_closed in Hs. }
          { erewrite on_free_vars_subst_instance.
            eapply subject_closed in Hs; rewrite is_open_term_closed in Hs.
            now rewrite on_free_vars_subst_instance in Hs. }
          destruct pb; apply eq_term_upto_univ_subst_instance; try typeclasses eauto; auto. }
Qed.

Lemma is_closed_context_subst_instance Γ Δ u :
  is_closed_context (Γ ,,, Δ @[u]) = is_closed_context (Γ ,,, Δ).
Proof.
  rewrite !on_free_vars_ctx_app. eauto with fvs.
Qed.

Lemma is_open_term_subst_instance Γ Δ t u u' :
  is_open_term (Γ ,,, Δ @[u]) t@[u'] = is_open_term (Γ ,,, Δ) t.
Proof.
  rewrite !app_context_length; len. eauto with fvs.
Qed.
#[global]
Hint Rewrite is_closed_context_subst_instance is_open_term_subst_instance : fvs.

Lemma eq_term_compare_term {cf} pb Σ t u :
  eq_term Σ Σ t u
  compare_term pb Σ Σ t u.
Proof.
  destruct pb; cbn; auto.
  now apply eq_term_leq_term.
Qed.

Lemma subst_instance_ws_cumul_ctx_pb_rel {cf:checker_flags} {Σ} {wfΣ : wf Σ} {Γ Δ u u' pb} :
  is_closed_context (Γ ,,, Δ)
  R_universe_instance (eq_universe Σ) u u'
  ws_cumul_ctx_pb_rel pb Σ Γ (subst_instance u Δ) (subst_instance u' Δ).
Proof.
  moveequ.
  split; eauto with fvs.
  { rewrite on_free_vars_ctx_app in equ. now move/andP: equ. }
  induction Δ as [|d Δ].
  - constructor.
  - simpl.
    destruct d as [na [b|] ty] ⇒ /=.
    × move: equ; rewrite /= on_free_vars_ctx_snoc ⇒ /= /andP[] clΔ /andP[] /= onb onty.
      rewrite !subst_instance_cons; constructor; eauto. simpl. constructor.
      + reflexivity.
      + constructor; cbn.
        4:eapply eq_term_upto_univ_subst_instance; try typeclasses eauto; auto.
        all:eauto with fvs.
      + constructor.
        4:cbn; eapply eq_term_compare_term;
          eapply eq_term_upto_univ_subst_instance; try typeclasses eauto; auto.
        all:eauto with fvs.
    × move: equ; rewrite /= on_free_vars_ctx_snoc ⇒ /= /andP[] clΔ /andP[] /= onb onty.
      rewrite !subst_instance_cons; constructor; eauto. simpl. constructor.
      + reflexivity.
      + cbn. constructor; auto.
        4:cbn; eapply eq_term_compare_term;
        eapply eq_term_upto_univ_subst_instance; try typeclasses eauto; auto.
        all:eauto with fvs.
Qed.

Lemma All2_fold_over_same {cf:checker_flags} Σ Γ Δ Δ' :
  All2_fold (fun Γ0 Γ'conv_decls cumulAlgo_gen Σ (Γ ,,, Γ0) (Γ ,,, Γ')) Δ Δ'
  All2_fold (conv_decls cumulAlgo_gen Σ) (Γ ,,, Δ) (Γ ,,, Δ').
Proof.
  induction 1; simpl; try constructor; pcuic.
Qed.

Lemma All2_fold_over_same_app {cf:checker_flags} Σ Γ Δ Δ' :
  All2_fold (conv_decls cumulAlgo_gen Σ) (Γ ,,, Δ) (Γ ,,, Δ')
  All2_fold (fun Γ0 Γ'conv_decls cumulAlgo_gen Σ (Γ ,,, Γ0) (Γ ,,, Γ')) Δ Δ'.
Proof.
  moveH. pose (All2_fold_length H).
  autorewrite with len in e. assert(#|Δ| = #|Δ'|) by lia.
  move/All2_fold_app_inv: HH.
  now specialize (H H0) as [_ H].
Qed.

Lemma eq_term_inds {cf:checker_flags} (Σ : global_env_ext) u u' ind mdecl :
  R_universe_instance (eq_universe (global_ext_constraints Σ)) u u'
  All2 (eq_term Σ Σ) (inds (inductive_mind ind) u (ind_bodies mdecl))
    (inds (inductive_mind ind) u' (ind_bodies mdecl)).
Proof.
  moveequ.
  unfold inds. generalize #|ind_bodies mdecl|.
  induction n; constructor; auto.
  clear IHn.
  repeat constructor. destruct ind; simpl in ×.
  eapply (R_global_instance_empty_impl _ _ _ _ _ _ 0).
  4:{ unfold R_global_instance. simpl. eauto. }
  all:typeclasses eauto.
Qed.

Lemma conv_inds {cf:checker_flags} (Σ : global_env_ext) Γ u u' ind mdecl :
  R_universe_instance (eq_universe (global_ext_constraints Σ)) u u'
  is_closed_context Γ
  ws_cumul_pb_terms Σ Γ (inds (inductive_mind ind) u (ind_bodies mdecl))
    (inds (inductive_mind ind) u' (ind_bodies mdecl)).
Proof.
  moveequ.
  unfold inds. generalize #|ind_bodies mdecl|.
  induction n; constructor; auto.
  clear IHn.
  repeat constructor; auto. destruct ind; simpl in ×.
  eapply (R_global_instance_empty_impl _ _ _ _ _ _ 0).
  4:{ unfold R_global_instance. simpl. eauto. }
  all:typeclasses eauto.
Qed.

Lemma R_global_instance_length Σ Req Rle ref napp i i' :
  R_global_instance Σ Req Rle ref napp i i' #|i| = #|i'|.
Proof.
  unfold R_global_instance.
  destruct global_variance.
  { induction i in l, i' |- *; destruct l, i'; simpl; auto; try lia; try easy.
    × specialize (IHi i' []). simpl in IHi. intuition.
    × intros []. intuition.
    }
  { unfold R_universe_instance.
    intros H % Forall2_length. now rewrite !map_length in H. }
Qed.

Lemma R_universe_instance_variance_irrelevant Re Rle i i' :
  #|i| = #|i'|
  R_universe_instance_variance Re Rle [] i i'.
Proof.
  now induction i in i' |- *; destruct i'; simpl; auto.
Qed.

Lemma ws_cumul_pb_it_mkProd_or_LetIn {cf pb Σ} {wfΣ : wf Σ} (Δ Γ Γ' : context) (B B' : term) :
  ws_cumul_ctx_pb_rel Conv Σ Δ Γ Γ'
  Σ ;;; Δ ,,, Γ B ≤[pb] B'
  Σ ;;; Δ it_mkProd_or_LetIn Γ B ≤[pb] it_mkProd_or_LetIn Γ' B'.
Proof.
  intros [_ cv].
  move: B B' Γ' Δ cv.
  induction Γ as [|d Γ] using rev_ind; moveB B' Γ' Δ;
  destruct Γ' as [|d' Γ'] using rev_ind; try clear IHΓ';
    moveH; try solve [simpl; auto].
  + depelim H. apply app_eq_nil in H; intuition discriminate.
  + depelim H. apply app_eq_nil in H; intuition discriminate.
  + assert (clen : #|Γ| = #|Γ'|).
    { apply All2_fold_length in H.
      autorewrite with len in H; simpl in H. lia. }
    apply All2_fold_app_inv in H as [cd cctx] ⇒ //.
    depelim cd; depelim a.
    - rewrite !it_mkProd_or_LetIn_app ⇒ //=.
      simpl. moveHB. apply ws_cumul_pb_Prod ⇒ /= //.
      eapply IHΓ.
      × unshelve eapply (All2_fold_impl cctx).
        simpl. intros ? ? × X. now rewrite !app_context_assoc in X.
      × now rewrite app_context_assoc in HB.
    - rewrite !it_mkProd_or_LetIn_app ⇒ //=.
      simpl. intros HB. cbn. apply ws_cumul_pb_LetIn ⇒ //; auto.
      eapply IHΓ.
      × unshelve eapply (All2_fold_impl cctx).
        simpl. intros ?? × X. now rewrite !app_context_assoc in X.
      × now rewrite app_context_assoc in HB.
Qed.

Lemma ws_cumul_pb_rel_it_mkLambda_or_LetIn {cf pb Σ} {wfΣ : wf Σ} (Δ Γ Γ' : context) (B B' : term) :
  ws_cumul_ctx_pb_rel Conv Σ Δ Γ Γ'
  Σ ;;; Δ ,,, Γ B ≤[pb] B'
  Σ ;;; Δ it_mkLambda_or_LetIn Γ B ≤[pb] it_mkLambda_or_LetIn Γ' B'.
Proof.
  move/ws_cumul_ctx_pb_rel_apphc hb.
  now eapply ws_cumul_pb_it_mkLambda_or_LetIn.
Qed.

Section ConvTerms.
  Context {cf} {Σ} {wfΣ : wf Σ}.

  Lemma ws_cumul_pb_terms_alt {Γ args args'} :
    ws_cumul_pb_terms Σ Γ args args' <~>
     argsr argsr',
       All2 (closed_red Σ Γ) args argsr,
      All2 (closed_red Σ Γ) args' argsr' &
      All2 (eq_term Σ Σ) argsr argsr'].
  Proof using wfΣ.
    split.
    - intros conv.
      induction conv.
      + [], []; eauto with pcuic.
      + apply ws_cumul_pb_red in r as (xr&yr&[xred yred xy]).
        specialize IHconv as (argsr&argsr'&[]).
         (xr :: argsr), (yr :: argsr').
        eauto 7 with pcuic.
    - intros (argsr&argsr'& [r r' eqs]).
      induction eqs in args, args', r, r' |- *; depelim r; depelim r'; [constructor|].
      constructor; auto.
      apply ws_cumul_pb_red; eauto.
  Qed.

  Lemma ws_cumul_pb_terms_ws_cumul_ctx {Γ Γ' ts ts'} :
    Σ Γ = Γ'
    ws_cumul_pb_terms Σ Γ ts ts'
    ws_cumul_pb_terms Σ Γ' ts ts'.
  Proof using wfΣ.
    intros ctx conv.
    induction conv; [constructor|].
    constructor; auto.
    eapply PCUICContextConversion.ws_cumul_pb_ws_cumul_ctx_inv; eauto.
  Qed.

  Lemma ws_cumul_pb_terms_red {Γ ts ts' tsr tsr'} :
    All2 (closed_red Σ Γ) ts tsr
    All2 (closed_red Σ Γ) ts' tsr'
    ws_cumul_pb_terms Σ Γ tsr tsr'
    ws_cumul_pb_terms Σ Γ ts ts'.
  Proof using wfΣ.
    intros all all' conv.
    induction conv in ts, ts', all, all' |- *; depelim all; depelim all'; [constructor|].
    constructor; [|auto].
    eapply red_ws_cumul_pb_left; tea.
    symmetry.
    eapply red_ws_cumul_pb_left; eauto.
    now symmetry.
  Qed.

  Lemma ws_cumul_pb_terms_red_inv {Γ ts ts' tsr tsr'} :
    All2 (closed_red Σ Γ) ts tsr
    All2 (closed_red Σ Γ) ts' tsr'
    ws_cumul_pb_terms Σ Γ ts ts'
    ws_cumul_pb_terms Σ Γ tsr tsr'.
  Proof using wfΣ.
    intros all all' conv.
    induction conv in tsr, tsr', all, all' |- *; depelim all; depelim all'; [constructor|].
    constructor; [|auto].
    eapply (ws_cumul_pb_red_l_inv x); eauto with fvs.
    symmetry.
    eapply (ws_cumul_pb_red_l_inv y0); eauto with fvs.
    now symmetry.
  Qed.

  Lemma ws_cumul_pb_terms_red_conv {Γ Γ' ts ts' tsr tsr'} :
    Σ Γ = Γ'
    All2 (closed_red Σ Γ) ts tsr
    All2 (closed_red Σ Γ') ts' tsr'
    ws_cumul_pb_terms Σ Γ tsr tsr'
    ws_cumul_pb_terms Σ Γ ts ts'.
  Proof using wfΣ.
    intros convctx all all2 conv.
    transitivity tsr.
    { solve_all. now eapply red_conv. }
    symmetry.
    transitivity tsr'.
    { solve_all. eapply ws_cumul_pb_ws_cumul_ctx; tea.
      now eapply red_conv. }
    now symmetry.
  Qed.

  Lemma ws_cumul_pb_terms_weaken {Γ Γ' args args'} :
    wf_local Σ Γ
    wf_local Σ Γ'
    ws_cumul_pb_terms Σ Γ args args'
    ws_cumul_pb_terms Σ (Γ' ,,, Γ) args args'.
  Proof using wfΣ.
    intros wf wf' conv.
    solve_all.
    eapply weaken_ws_cumul_pb; eauto with fvs.
  Qed.

  Lemma ws_cumul_pb_terms_subst {Γ Γ' Γ'' Δ s s' args args'} :
    is_closed_context (Γ ,,, Γ'')
    untyped_subslet Γ s Γ'
    untyped_subslet Γ s' Γ''
    ws_cumul_pb_terms Σ Γ s s'
    ws_cumul_pb_terms Σ (Γ ,,, Γ' ,,, Δ) args args'
    ws_cumul_pb_terms Σ (Γ ,,, subst_context s 0 Δ) (map (subst s #|Δ|) args) (map (subst s' #|Δ|) args').
  Proof using wfΣ.
    intros wf cl cl' convs conv.
    eapply All2_map.
    eapply (All2_impl conv).
    intros x y eqxy.
    eapply substitution_ws_cumul_pb_subst_conv; eauto with fvs.
  Qed.

End ConvTerms.

Section CumulSubst.
  Context {cf} {Σ} {wfΣ : wf Σ}.

  Lemma untyped_substitution_ws_cumul_pb_subst_conv' {pb Γ Δ Δ' Γ' s s' b} :
    is_closed_context (Γ ,,, Δ ,,, Γ')
    is_closed_context (Γ ,,, Δ')
    is_open_term (Γ ,,, Δ ,,, Γ') b
    ws_cumul_pb_terms Σ Γ s s'
    untyped_subslet Γ s Δ
    untyped_subslet Γ s' Δ'
    Σ ;;; Γ ,,, subst_context s 0 Γ' subst s #|Γ'| b ≤[pb] subst s' #|Γ'| b.
  Proof using wfΣ.
    movecl cl' clb eqsub subs subs'.
    eapply ws_cumul_pb_eq_le_gen.
    eapply substitution_ws_cumul_pb_subst_conv; tea; eauto with pcuic.
  Qed.

  Lemma substitution_ws_cumul_ctx_pb_subst_conv {Γ Γ' Γ'0 Γ'' Δ Δ' s s' pb} :
    ws_cumul_ctx_pb_rel pb Σ (Γ ,,, Γ' ,,, Γ'') Δ Δ'
    ws_cumul_pb_terms Σ Γ s s'
    untyped_subslet Γ s Γ'
    untyped_subslet Γ s' Γ'0
    is_closed_context (Γ ,,, Γ'0)
    ws_cumul_ctx_pb_rel pb Σ (Γ ,,, subst_context s 0 Γ'') (subst_context s #|Γ''| Δ) (subst_context s' #|Γ''| Δ').
  Proof using wfΣ.
    intros [cl cum] eqs hs hs' cl'.
    split.
    { eapply is_closed_subst_context; tea; eauto with fvs.
      apply (untyped_subslet_length hs). }
    eapply All2_fold_fold_context_k.
    eapply All2_fold_impl_ind; tea. clear cum.
    moveΔ0 Δ'0 d d'; cbn ⇒ /All2_fold_length len _ ad.
    eapply All_decls_alpha_pb_map.
    eapply All_decls_alpha_pb_impl; tea.
    intros pb' x y; cbnleq.
    rewrite -/(subst_context _ _ _).
    rewrite -app_context_assoc (subst_context_app0 s Γ'' Δ0).
    rewrite - !app_length.
    relativize #|Δ'0 ++ Γ''|; [apply (substitution_ws_cumul_pb_subst_conv (pb:=pb') hs hs' eqs)|] ⇒ //.
    1:rewrite app_context_assoc //.
    len.
  Qed.

  Lemma weaken_ws_cumul_ctx_pb_rel {pb Γ Γ' Δ Δ'} :
    is_closed_context Γ
    ws_cumul_ctx_pb_rel pb Σ Γ' Δ Δ'
    ws_cumul_ctx_pb_rel pb Σ (Γ ,,, Γ') Δ Δ'.
  Proof using wfΣ.
    intros wf [cl eq].
    split.
    { rewrite on_free_vars_ctx_app wf /=.
      eapply on_free_vars_ctx_impl; tea ⇒ //.
      congruence. }
    induction eq.
    - simpl. constructor.
    - constructor; auto.
      eapply All_decls_alpha_pb_impl; tea.
      move⇒ /= le' x y c.
      rewrite -app_context_assoc.
      eapply weaken_ws_cumul_pb; tea; eauto with fvs.
  Qed.

Local Open Scope sigma_scope.

Lemma map_branches_k_map_branches_k
      (f : nat term term) k
      (f' : nat term term) k'
      (l : list (branch term)) :
  map_branches_k f id k (map_branches_k f' id k' l) =
  map (map_branch_k (fun (i : nat) (x : term) ⇒ f (i + k) (f' (i + k') x)) id 0) l.
Proof using Type.
  rewrite map_map.
  eapply map_extb.
  rewrite map_branch_k_map_branch_k; auto.
Qed.

Lemma red_rel_all {Γ i body t} :
  option_map decl_body (nth_error Γ i) = Some (Some body)
  red Σ Γ t (lift 1 i (t {i := body})).
Proof using Type.
  induction t using PCUICInduction.term_forall_list_ind in Γ, i |- *; intro H; cbn;
    eauto using red_prod, red_abs, red_app, red_letin, red_proj_c.
  - case_eq (i <=? n); intro H0.
    + apply Nat.leb_le in H0.
      case_eq (n - i); intros; cbn.
      × apply red1_red.
        assert (n = i) by lia; subst.
        rewrite simpl_lift; cbn; try lia.
        now constructor.
      × enough (nth_error (@nil term) n0 = None) as ->;
          [cbn|now destruct n0].
        enough (i <=? n - 1 = true) as ->; try (apply Nat.leb_le; lia).
        enough (S (n - 1) = n) as ->; try lia. auto.
    + cbn. rewrite H0. auto.
  - eapply red_evar. repeat eapply All2_map_right.
    eapply All_All2; tea. intro; cbn; eauto.
  - destruct X as (IHparams&IHctx&IHret).
    rewrite map_predicate_k_map_predicate_k.
    assert (ctxapp: Γ',
               option_map decl_body (nth_error (Γ,,, Γ') (#|Γ'| + i)) = Some (Some body)).
    { unfold app_context.
      intros.
      rewrite nth_error_app2; [lia|].
      rewrite Nat.add_comm Nat.add_sub; auto. }
    eapply red_case.
    + induction IHparams; pcuic.
    + apply IHret; auto.
      rewrite nth_error_app_ge ?inst_case_predicate_context_length; try lia.
      rewrite -H. lia_f_equal.
    + eapply IHt; auto.
    + clear -wfΣ X0 ctxapp.
      induction X0; pcuic.
      constructor; auto.
      unfold on_Trel.
      rewrite map_branch_k_map_branch_k ⇒ //.
      split.
      × eapply b.
        rewrite Nat.add_0_r.
        eauto.
        rewrite nth_error_app_ge ?inst_case_branch_context_length; try lia.
        rewrite -(ctxapp []) /=. lia_f_equal.
      × cbn. auto.
  - eapply red_fix_congr. repeat eapply All2_map_right.
    eapply All_All2; tea. intros; cbn in *; rdest; eauto.
    rewrite map_length. eapply r0.
    rewrite nth_error_app_context_ge; rewrite fix_context_length; try lia.
    enough (#|m| + i - #|m| = i) as ->; tas; lia.
  - eapply red_cofix_congr. repeat eapply All2_map_right.
    eapply All_All2; tea. intros; cbn in *; rdest; eauto.
    rewrite map_length. eapply r0.
    rewrite nth_error_app_context_ge; rewrite fix_context_length; try lia.
    enough (#|m| + i - #|m| = i) as ->; tas; lia.
Qed.

Lemma closed_red_rel_all {Γ i body t} :
  is_closed_context Γ
  is_open_term Γ t
  option_map decl_body (nth_error Γ i) = Some (Some body)
  Σ ;;; Γ t lift 1 i (t {i := body}).
Proof using Type.
  intros cl clt h; split; auto.
  now apply red_rel_all.
Qed.

End CumulSubst.

Section MoreCongruenceLemmas.

  Context {cf:checker_flags} (Σ : global_env_ext) (wfΣ : wf Σ).

  Lemma red_terms_evar Γ args args0 ev :
    red_terms Σ Γ args args0 red Σ Γ (tEvar ev args) (tEvar ev args0).
    intros Hargs. eapply red_evar.
    eapply All2_impl. 1: tea. intros. destruct X; eauto.
  Defined.

  Lemma ws_cumul_pb_Evar {pb Γ ev args args'} :
    ws_cumul_pb_terms Σ Γ args args' is_closed_context Γ
    Σ;;; Γ tEvar ev args ≤[pb] tEvar ev args'.
  Proof.
    intros Hargsargs' . pose proof (Hargs := ws_cumul_pb_terms_open_terms_left Hargsargs'). pose proof (Hargs' := ws_cumul_pb_terms_open_terms_right Hargsargs').
    apply ws_cumul_pb_terms_alt in Hargsargs'. destruct Hargsargs' as [args0 [args0' [Hargs0 Hargs0' Hargs0args0']]].
    pose proof (Hargs0_c := closed_red_terms_open_right Hargs0).
    pose proof (Hargs0'_c := closed_red_terms_open_right Hargs0').
    assert (Σ;;; Γ tEvar ev args0 ≤[pb] tEvar ev args0').
    { econstructor; eauto; cbn. 3: econstructor; eauto.
      all: eapply All_forallb; eauto. }
    eapply red_terms_evar with (ev := ev)in Hargs0.
    eapply red_terms_evar with (ev := ev)in Hargs0'.
    eapply red_ws_cumul_pb_left in X. 2: split; eauto; cbn; eauto.
    eapply red_ws_cumul_pb_right in X. 2: split; eauto; cbn; eauto.
    exact X.
  Defined.

  Lemma ws_cumul_pb_Ind {pb Γ ind ui ui' l l'} :
   R_global_instance Σ (eq_universe Σ) (compare_universe pb Σ) (IndRef ind) #|l| ui ui',
      is_closed_context Γ & ws_cumul_pb_terms Σ Γ l l']
  Σ ;;; Γ mkApps (tInd ind ui) l ≤[pb] mkApps (tInd ind ui') l'.
    intros [Rglob Rclosed Hll']. apply ws_cumul_pb_terms_alt in Hll'. destruct Hll' as [l0 [l0' [Hl0 Hl0' Hl0l0']]].
    assert (Σ ;;; Γ mkApps (tInd ind ui) l0 ≤[pb] mkApps (tInd ind ui') l0').
    { econstructor 1; eauto.
      - cbn. clear -cf wfΣ Hl0. rewrite on_free_vars_mkApps; cbn. apply All_forallb. induction Hl0; eauto; intros. cbn in ×. econstructor; eauto.
        destruct r; eapply red_is_open_term; eauto.
      - cbn. clear -cf wfΣ Hl0'. rewrite on_free_vars_mkApps; cbn. apply All_forallb. induction Hl0'; eauto; intros. cbn in ×. econstructor; eauto.
        destruct r; eapply red_is_open_term; eauto.
      - apply All2_length in Hl0. rewrite Hl0 in Rglob. clear Hl0 Hl0'.
        apply eq_term_upto_univ_napp_mkApps; eauto.
        econstructor; eauto. assert (#|l0| + 0 = #|l0|) by lia. rewrite H. destruct pb; eauto.
    }
    apply red_terms_ws_cumul_pb_terms in Hl0, Hl0'.
    etransitivity.
    - eapply ws_cumul_pb_mkApps.
      × refine (ws_cumul_pb_refl' (exist Γ Rclosed) (exist (tInd ind ui) _)); eauto.
      × eassumption.
    - cbn. etransitivity; try apply X.
      eapply ws_cumul_pb_mkApps.
      × refine (ws_cumul_pb_refl' (exist Γ Rclosed) (exist (tInd ind ui') _)); eauto.
      × symmetry. eassumption.
  Defined.

  Lemma ws_cumul_pb_Construct {pb Γ i k ui ui' l l'} :
   R_global_instance Σ (eq_universe Σ) (compare_universe pb Σ) (ConstructRef i k) #|l| ui ui',
     is_closed_context Γ & ws_cumul_pb_terms Σ Γ l l']
  Σ ;;; Γ mkApps (tConstruct i k ui) l ≤[pb] mkApps (tConstruct i k ui') l'.
  intros [Rglob Rclosed Hll']. apply ws_cumul_pb_terms_alt in Hll'. destruct Hll' as [l0 [l0' [Hl0 Hl0' Hl0l0']]].
  assert (Σ ;;; Γ mkApps (tConstruct i k ui) l0 ≤[pb] mkApps (tConstruct i k ui') l0').
  { econstructor 1; eauto.
    - cbn. clear -cf wfΣ Hl0. rewrite on_free_vars_mkApps; cbn. apply All_forallb. induction Hl0; eauto; intros. cbn in ×. econstructor; eauto.
      destruct r; eapply red_is_open_term; eauto.
    - cbn. clear -cf wfΣ Hl0'. rewrite on_free_vars_mkApps; cbn. apply All_forallb. induction Hl0'; eauto; intros. cbn in ×. econstructor; eauto.
      destruct r; eapply red_is_open_term; eauto.
    - apply All2_length in Hl0. rewrite Hl0 in Rglob. clear Hl0 Hl0'.
      apply eq_term_upto_univ_napp_mkApps; eauto.
      econstructor; eauto. assert (#|l0| + 0 = #|l0|) by lia. rewrite H. destruct pb; eauto.
  }
  apply red_terms_ws_cumul_pb_terms in Hl0, Hl0'.
  etransitivity.
  - eapply ws_cumul_pb_mkApps.
    × refine (ws_cumul_pb_refl' (exist Γ Rclosed) (exist (tConstruct i k ui) _)); eauto.
    × eassumption.
  - cbn. etransitivity; try apply X.
    eapply ws_cumul_pb_mkApps.
    × refine (ws_cumul_pb_refl' (exist Γ Rclosed) (exist (tConstruct i k ui') _)); eauto.
    × symmetry. eassumption.
Defined.

End MoreCongruenceLemmas.

Section CumulSpecIsCumulAlgo.

Context {cf:checker_flags} (Σ : global_env_ext) (wfΣ : wf Σ).

Lemma on_free_vars_ctx_inst_case_context_xpred0 (Γ : list context_decl) (pars : list term)
  (puinst : Instance.t) (pctx : list context_decl) :
  forallb (on_free_vars (shiftnP #|Γ| xpred0)) pars
  on_free_vars_ctx (closedP #|pars| xpredT) pctx
  on_free_vars_ctx xpred0 Γ
  on_free_vars_ctx xpred0 (Γ,,, inst_case_context pars puinst pctx).
Proof using Type.
  intros. rewrite on_free_vars_ctx_app H1 /=.
  eapply on_free_vars_ctx_inst_case_context; trea; solve_all.
  rewrite test_context_k_closed_on_free_vars_ctx //.
Qed.

Proposition cumulSpec_cumulAlgo {pb} (Γ : closed_context) (M N : open_term Γ) :
  Σ ;;; Γ M s[pb] N
  Σ ;;; Γ M ≤[pb] N.
Proof.
  destruct Γ as [Γ ], M as [M HM], N as [N HN] ; cbn in ×.
  unfold cumulSpec in ×.
  intros e.
  revert pb Γ M N e HM HN.
  apply: (cumulSpec0_ind_all Σ).
  1-9: intros; subst; econstructor 2; eauto; try solve [econstructor; eauto];
    match goal with |- _ ;;; _ ?t ≤[_] _
      eapply (ws_cumul_pb_refl' (exist Γ _) (exist t _)) end.
  all: intro pb.
  - intros; etransitivity; eauto.
  - intros. apply ws_cumul_pb_eq_le_gen. apply symmetry.
    now apply X0.
  - intros Γ t; intros. unshelve eapply (ws_cumul_pb_refl' (exist Γ _) (exist t _)); eauto.
  - intros Γ ev args args' Hargsargs' Hargs Hargs'. cbn in ×. eapply ws_cumul_pb_Evar; eauto.
    apply forallb_All in Hargs, Hargs'. apply (All2_All_mix_left Hargs) in Hargsargs'. clear Hargs.
    apply (All2_All_mix_right Hargs') in Hargsargs'. clear Hargs'. eapply All2_impl. 1: tea. cbn; intros x y [[Hx Heqxy ] Hy].
    eapply Heqxy; eauto.
  - intros Γ t t' u u' Htt' Heqtt' Huu' Hequu' HM HN. cbn in *; apply andb_andI in HM; apply andb_andI in HN; destruct HM as [Ht Hu]; destruct HN as [Ht' Hu'].
    eapply ws_cumul_pb_App; eauto.
  - intros Γ na na' ty ty' t t' Hna Htyty' Heqtyty' Htt' Heqtt' HM HN.
    cbn in ×. apply andb_andI in HM; apply andb_andI in HN; destruct HM as [Hty Ht]; destruct HN as [Hty' Ht'].
    eapply ws_cumul_pb_Lambda; eauto. eapply Heqtt'; eauto.
    × change (is_closed_context (Γ,, vass na ty)). rewrite on_free_vars_ctx_snoc. apply andb_and. split; eauto.
    × rewrite shiftnP_S; eauto.
    × rewrite shiftnP_S; eauto.
  - intros Γ na na' a a' b b' Hna Haa' foo IHe1 IHe2 HM HN. cbn in *; apply andb_andI in HM; apply andb_andI in HN; destruct HM as [Ha Hb]; destruct HN as [Ha' Hb'].
    eapply ws_cumul_pb_Prod; eauto. eapply IHe2; eauto.
    × change (is_closed_context (Γ,, vass na a)). rewrite on_free_vars_ctx_snoc. apply andb_and. split; eauto.
    × rewrite shiftnP_S; eauto.
    × rewrite shiftnP_S; eauto.
  - intros Γ na na' t t' ty ty' u u' Hna _ Heqtt' _ Heqtyty' _ Hequu' HM HN.
    cbn in ×. apply andb_andI in HM; apply andb_andI in HN; destruct HM as [Ht Htyu]; destruct HN as [Ht' Htyu'].
    apply andb_andI in Htyu; apply andb_andI in Htyu'; destruct Htyu as [Hty Hu]; destruct Htyu' as [Hty' Hu'].
    eapply ws_cumul_pb_LetIn; eauto. eapply Hequu'; eauto.
    × change (is_closed_context (Γ,, vdef na t ty)). rewrite on_free_vars_ctx_snoc. apply andb_and. split; eauto.
      rewrite /on_free_vars_decl /test_decl. apply andb_and. split; eauto.
    × rewrite shiftnP_S; eauto.
    × rewrite shiftnP_S; eauto.
  - intros Γ indn p p' c c' brs brs' Hpp' _ Hcc' Hbrsbrs' H H'.
    cbn in ×. apply andb_andI in H; apply andb_andI in H'; destruct H as [Hp H]; destruct H' as [Hp' H'].
    apply andb_andI in H; apply andb_andI in H'; destruct H as [Hreturn H]; destruct H' as [Hreturn' H'].
    apply andb_andI in H; apply andb_andI in H'; destruct H as [Hcontext H]; destruct H' as [Hcontext' H'].
    apply andb_andI in H; apply andb_andI in H'; destruct H as [Hc Hbrs]; destruct H' as [Hc' Hbrs'].
    eapply ws_cumul_pb_eq_le_gen. eapply ws_cumul_pb_Case; eauto.
    × rewrite is_open_case_split. repeat (apply andb_and; split); eauto.
    × rewrite is_open_case_split. repeat (apply andb_and; split); eauto.
    × unfold cumul_predicate in Hpp'. unfold ws_cumul_pb_predicate. destruct Hpp' as [Hpp' [Hinst [Hpcon Hpret]]].
      split; eauto.
      + clear - Hp Hp' Hpp' . apply forallb_All in Hp, Hp'.
        apply (All2_All_mix_left Hp) in Hpp'. clear Hp.
        apply (All2_All_mix_right Hp') in Hpp'. clear Hp'.
        eapply All2_impl. 1: tea. cbn; intros x y [[Hx Heqxy ] Hy].
        eapply Heqxy.2; eauto.
      + eapply Hpret; eauto.
        ++ rewrite test_context_k_closed_on_free_vars_ctx in Hcontext.
           unfold inst_case_predicate_context. apply PCUICOnFreeVarsConv.on_free_vars_ctx_inst_case_context ; eauto.
        ++ rewrite shiftnP_add in Hreturn. rewrite <- inst_case_predicate_context_length in Hreturn.
          rewrite <- app_length in Hreturn. eassumption.
        ++ rewrite shiftnP_add in Hreturn'. rewrite <- (All2_fold_length Hpcon) in Hreturn'.
           rewrite <- inst_case_predicate_context_length in Hreturn'.
           rewrite <- app_length in Hreturn'. eassumption.
    × unfold ws_cumul_pb_brs. clear - Hp Hp' Hbrs Hbrs' Hbrsbrs'.
      apply forallb_All in Hbrs, Hbrs'. apply (All2_All_mix_left Hbrs) in Hbrsbrs'. clear Hbrs.
      apply (All2_All_mix_right Hbrs') in Hbrsbrs'. clear Hbrs'. eapply All2_impl. 1: tea. cbn; intros x y [[Hx Heqxy ] Hy].
      split; try apply Heqxy.1. clear Hbrsbrs'. rewrite test_context_k_closed_on_free_vars_ctx in Hx. toProp Hx.
      rewrite test_context_k_closed_on_free_vars_ctx in Hy. toProp Hy. eapply Heqxy.2; eauto.
      + apply PCUICOnFreeVarsConv.on_free_vars_ctx_inst_case_context ; eauto; intuition.
      + rewrite shiftnP_add in Hx. erewrite <- inst_case_branch_context_length in Hx.
        rewrite <- app_length in Hx. intuition.
      + rewrite shiftnP_add in Hy. rewrite <- (All2_fold_length Heqxy.1.1) in Hy. erewrite <- inst_case_branch_context_length in Hy.
        rewrite <- app_length in Hy. intuition.
  - intros; eapply ws_cumul_pb_Proj_c; eauto.
  - intros Γ mfix mfix' idx Hmfixmfix' H H'. cbn in ×.
    eapply ws_cumul_pb_eq_le_gen. eapply ws_cumul_pb_Fix; eauto. apply forallb_All in H, H'.
    apply (All2_All_mix_left H) in Hmfixmfix'.
    apply (All2_All_mix_right H') in Hmfixmfix'.
    eapply All2_impl. 1: tea. pose proof (Hfix := All2_length Hmfixmfix'); clear Hmfixmfix'; cbn; intros. destruct X as [[Hx [[ [_ [rtype _]] [rbody rargs]] rname]] Hy].
    apply andb_andI in Hx; apply andb_andI in Hy; destruct Hx as [Hdtypex Hdbodyx]; destruct Hy as [Hdtypey Hdbodyy].
    repeat split; eauto. eapply rbody; eauto.
    × rewrite on_free_vars_ctx_app; solve_all. rewrite on_free_vars_fix_context; eauto.
    × rewrite shiftnP_add in Hdbodyx. erewrite <- fix_context_length in Hdbodyx.
      rewrite <- app_length in Hdbodyx. intuition.
    × rewrite shiftnP_add in Hdbodyy. rewrite <- Hfix in Hdbodyy. erewrite <- fix_context_length in Hdbodyy.
      rewrite <- app_length in Hdbodyy. intuition.
  - intros Γ mfix mfix' idx Hmfixmfix' H H'. cbn in ×.
    eapply ws_cumul_pb_eq_le_gen. eapply ws_cumul_pb_CoFix; eauto. apply forallb_All in H, H'.
    apply (All2_All_mix_left H) in Hmfixmfix'.
    apply (All2_All_mix_right H') in Hmfixmfix'.
    eapply All2_impl. 1: tea. pose proof (Hfix := All2_length Hmfixmfix'); clear Hmfixmfix'; cbn; intros. destruct X as [[Hx [[ [_ [rtype _]] [rbody rargs]] rname]] Hy].
    apply andb_andI in Hx; apply andb_andI in Hy; destruct Hx as [Hdtypex Hdbodyx]; destruct Hy as [Hdtypey Hdbodyy].
    repeat split; eauto. eapply rbody; eauto.
    × rewrite on_free_vars_ctx_app; solve_all. rewrite on_free_vars_fix_context; eauto.
    × rewrite shiftnP_add in Hdbodyx. erewrite <- fix_context_length in Hdbodyx.
      rewrite <- app_length in Hdbodyx. intuition.
    × rewrite shiftnP_add in Hdbodyy. rewrite <- Hfix in Hdbodyy. erewrite <- fix_context_length in Hdbodyy.
      rewrite <- app_length in Hdbodyy. intuition.
  - intros Γ i u u' args args' H X H0 H1 H2. eapply ws_cumul_pb_Ind; eauto. split; eauto.
    rewrite on_free_vars_mkApps in H1. rewrite on_free_vars_mkApps in H2.
    apply andb_and in H1, H2. destruct H1, H2. clear -X H0 H3 H4.
    apply forallb_All in H3, H4. apply (All2_All_mix_left H3) in X. clear H3.
    apply (All2_All_mix_right H4) in X. clear H4. eapply All2_impl. 1: tea. cbn; intros x y [[Hx Heqxy] Hy].
    eapply Heqxy.2; eauto.
  - intros Γ i k u u' args args' H X H0 H1 H2. eapply ws_cumul_pb_Construct; eauto ; split; eauto.
    rewrite on_free_vars_mkApps in H1. rewrite on_free_vars_mkApps in H2.
    apply andb_and in H1, H2. destruct H1, H2. clear -X H0 H3 H4.
    apply forallb_All in H3, H4. apply (All2_All_mix_left H3) in X. clear H3.
    apply (All2_All_mix_right H4) in X. clear H4. eapply All2_impl. 1: tea. cbn; intros x y [[Hx Heqxy] Hy].
    eapply Heqxy.2; eauto.
  - intros. econstructor 1; eauto. destruct pb; subst; econstructor; eauto.
  - intros. econstructor 1; eauto. destruct pb; subst; econstructor; eauto.
  Unshelve. all: eauto.
Defined.

Proposition convSpec_convAlgo (Γ : closed_context) (M N : open_term Γ) :
  Σ ;;; Γ |- M =s N
  Σ ;;; Γ M = N.
Proof using wfΣ.
  apply cumulSpec_cumulAlgo.
Qed.

Lemma convSpec_convAlgo_curry (Γ : context) (M N : term) :
  is_closed_context Γ is_open_term Γ M is_open_term Γ N
  Σ ;;; Γ |- M =s N
  Σ ;;; Γ M = N.
Proof using wfΣ.
  intros clΓ clM clN.
  eapply (convSpec_convAlgo (exist Γ clΓ) (exist M clM) (exist N clN)).
Qed.

Lemma cumulSpec_cumulAlgo_curry (Γ : context) (M N : term) :
  is_closed_context Γ is_open_term Γ M is_open_term Γ N
  Σ ;;; Γ |- M s N
  Σ ;;; Γ M N.
Proof using wfΣ.
  intros clΓ clM clN.
  eapply (cumulSpec_cumulAlgo (exist Γ clΓ) (exist M clM) (exist N clN)).
Qed.
End CumulSpecIsCumulAlgo.

Lemma cumulSpec_typed_cumulAlgo {cf} {Σ} {wfΣ : wf Σ} {Γ : context} {t A B s} :
  Σ ;;; Γ |- t : A
  Σ ;;; Γ |- B : tSort s
  Σ ;;; Γ |- A s B
  Σ ;;; Γ A B.
Proof.
  intros ta tb. eapply cumulSpec_cumulAlgo_curry; eauto with fvs.
Qed.
#[global] Hint Immediate cumulSpec_typed_cumulAlgo : pcuic.