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 ×
        Σ;;;