Library MetaCoq.PCUIC.PCUICConversion

From Coq Require Import ssreflect ssrbool.
From MetaCoq.Template Require Import config utils.
From MetaCoq.PCUIC Require Import PCUICAst PCUICAstUtils PCUICTactics PCUICCases PCUICLiftSubst PCUICTyping PCUICOnOne
     PCUICSubstitution PCUICPosition PCUICCumulativity PCUICReduction PCUICOnFreeVars
     PCUICConfluence PCUICClosed PCUICClosedConv PCUICClosedTyp PCUICParallelReductionConfluence PCUICEquality
     PCUICSigmaCalculus PCUICContextReduction PCUICContextConversion
     PCUICWeakeningConv PCUICWeakeningTyp PCUICUnivSubst
     PCUICWellScopedCumulativity PCUICUnivSubstitutionConv PCUICInduction.

Require Import CRelationClasses CMorphisms.
Require Import Equations.Type.Relation Equations.Type.Relation_Properties.
Require Import Equations.Prop.DepElim.

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 y → x' 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 u ⇒ isFixApp f
  | tFix mfix idx ⇒ true
  | _ ⇒ 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).
    move⇒ e [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).
    move⇒ e [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.
  move⇒ Hu; 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.
  move⇒ onΓ 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Σ.
    move⇒ conv_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 : nat ⇒ on_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 : nat ⇒ on_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 : nat ⇒ on_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.
    move⇒ onpars' 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.
    move⇒ onpret' /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'].
    move⇒ cvp 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 x ⇒ True)) 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_length ⇒ onbody 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_length ⇒ onbody 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 ×
        Σ;;;