(* Distributed under the terms of the MIT license. *)
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.

(* TODO MOVE *)
Fixpoint isFixApp t : bool :=
  match t with
  | tApp f u => isFixApp f
  | tFix mfix idx => true
  | _ => false
  end.

(* TODO MOVE *)
Lemma isFixApp_mkApps :
  forall 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.
    exists (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.
      exists (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]].
      exists 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]].
      exists s'. split; auto. eapply into_closed_red; tea.
      eapply red_step with v; eauto with fvs.
    - depelim r. solve_discr.
  Qed.

  (* #[global]
  Instance red_decls_refl Γ Δ : Reflexive (red_decls Σ Γ Δ).
  Proof.
    intros x. apply red_decls_refl.
  Qed.

  #[global]
  Instance red_ctx_refl : Reflexive (All2_fold (fun Γ _ => All_decls (closed_red Σ Γ))).
  Proof.
    intros x. eapply All2_fold_refl. intros. apply All_decls_refl.
  Qed. *)

  (* Lemma clos_rt_monotone_hetero {A B} (R : relation A) (S : relation B) (f : A -> B) :
    (forall x y, R x y -> on_Trel S f x y) ->
    (forall x y, R x y -> inclusion (clos_refl_trans R) (clos_refl_trans S). *)

  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.

  (*Inductive closed_subslet (Γ : context) : list term -> context -> Type :=
  | closed_emptyslet : closed_subslet Γ [] []
  | closed_cons_let_ass Δ s na t T :
      closed_subslet Γ s Δ ->
      is_open_term Γ t ->
      closed_subslet Γ (t :: s) (Δ ,, vass na T)
  | closed_cons_let_def Δ s na t T :
      closed_subslet Γ s Δ ->
      is_open_term Γ (subst0 s t) ->
      closed_subslet Γ (subst0 s t :: s) (Δ ,, vdef na t T).

  Lemma closed_subslet_untyped_subslet {Γ s Δ} :
    closed_subslet Γ s Δ ->
    untyped_subslet Γ s Δ.
  Proof.
    induction 1; constructor; auto.
  Qed.*)

  Hint Resolve untyped_subslet_length : pcuic.

  (* Lemma closed_red1_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.
    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_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.
      exists 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.

  (*Lemma ws_cumul_pb_LetIn_l_inv {Γ na d ty b T} :
    Σ ;;; Γ ⊢ tLetIn na d ty b ≤ T ->
    ∑ b', Σ ;;; Γ ⊢ T ⇝ b' × Σ ;;; Γ ⊢ b {0 := d} ≤ b'.
  Proof.
    intros H.
    eapply ws_cumul_pb_red in H as (v & v' & tv & tv' & eqp).
    exists v'. split; auto.
    destruct (invert_red_letin tv) as [(d' & ty' & b' & -> & redb & redty & redbod)|tv''].
    - cbn in eqp.
      etransitivity.
      2:{ eapply ws_cumul_pb_refl; tea; eauto with fvs. }
      transitivity (b' {0 := d'}).
      * transitivity (b' {0 := d}).
        + eapply red_ws_cumul_pb.
          eapply (closed_red_untyped_substitution0 (Δ := [_])); tea; cbn; eauto with pcuic fvs.
        + eapply red_ws_cumul_pb.
          eapply (closed_red_red_subst0 (Δ := [_])); eauto with fvs pcuic.
      * apply red_ws_cumul_pb_inv.
        split; eauto with fvs.
        eapply red1_red. constructor.
    - eapply ws_cumul_pb_red. exists v, v'.
      intuition pcuic. split; eauto with fvs.
  Qed.

  Lemma ws_cumul_pb_LetIn_r_inv {Γ na d ty b T} :
    Σ ;;; Γ ⊢ T ≤ tLetIn na d ty b ->
    ∑ b', Σ ;;; Γ ⊢ T ⇝ b' × Σ ;;; Γ ⊢ b' ≤ b {0 := d}.
  Proof.
    intros H.
    eapply ws_cumul_pb_red in H as (v & v' & tv & tv' & eqp).
    exists v. split; auto.
    destruct (invert_red_letin tv') as [(d' & ty' & b' & -> & redb & redty & redbod)|tv''].
    - cbn in eqp.
      etransitivity.
      1:{ eapply ws_cumul_pb_refl; tea; eauto with fvs. }
      eapply ws_cumul_pb_eq_le.
      transitivity (b' {0 := d'}).
      + eapply red_ws_cumul_pb. split; eauto with fvs.
        apply red1_red. constructor.
      + symmetry.
        transitivity (b' {0 := d}).
        * eapply red_ws_cumul_pb.
          eapply (closed_red_untyped_substitution0 (Δ := [_])); tea; cbn; eauto with pcuic fvs.
        * apply red_ws_cumul_pb.
          eapply (closed_red_red_subst0 (Δ := [_])); eauto with fvs pcuic.
    - eapply ws_cumul_pb_red. exists v, v'.
      intuition pcuic. 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'.
      exists 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'.
      exists 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'.
      exists 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'.
      exists 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 :=
    exists T', ∥ Σ ;;; Γ ⊢ T ⇝ T' ∥ /\ isArity T'.

  Lemma arity_red_to_prod_or_sort :
    forall Γ T,
      is_closed_context Γ ->
      is_open_term Γ T ->
      isArity T ->
      (exists na A B, ∥ Σ ;;; Γ ⊢ T ⇝ (tProd na A B) ∥) \/
      (exists 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 :
    forall Γ T,
      Is_conv_to_Arity Σ Γ T ->
      (exists na A B, ∥ Σ ;;; Γ ⊢ T ⇝ (tProd na A B) ∥) \/
      (exists 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 :
    forall 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]].
        exists (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]].
        exists (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 :
    forall 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]].
        exists (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]].
        exists (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 :
    forall 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 :
    forall Γ 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 :
    forall (Γ : 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']].
      exists 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 :
    forall (Γ : 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']].
      exists 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 :
    forall 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.
      exists 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]].
    exists args'; split => //.
    solve_all; split; eauto with fvs.
  Qed.

  (* TODO deprecate? #[deprecated(note="use red_mkApps_tInd")] *)
  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.

(* Unused... *)
(*Lemma it_mkProd_or_LetIn_ass_inv {cf : checker_flags} (Σ : global_env_ext) Γ ctx ctx' s s' :
  wf Σ ->
  assumption_context ctx ->
  assumption_context ctx' ->
  Σ ;;; Γ ⊢ it_mkProd_or_LetIn ctx (tSort s) ≤ it_mkProd_or_LetIn ctx' (tSort s') ->
  All2_fold (fun ctx ctx' => conv_decls Σ (Γ ,,, ctx) (Γ ,,, ctx')) ctx ctx' *
   leq_term Σ.1 Σ (tSort s) (tSort s').
Proof.
  intros.
  revert Γ ctx' s s'.
  induction ctx using rev_ind.
  - intros. destruct ctx' using rev_ind.
    + simpl in X.
      eapply cumul_Sort_inv in X.
      split; constructor; auto.
    + destruct x as [na [b|] ty].
      * elimtype False.
        apply assumption_context_app in H0.
        destruct H0. inv a0.
      * rewrite it_mkProd_or_LetIn_app in X.
        apply assumption_context_app in H0 as [H0 _].
        specialize (IHctx' H0).
        simpl in IHctx'. simpl in X.
        unfold mkProd_or_LetIn in X. simpl in X.
        eapply ws_cumul_pb_Sort_Prod_inv in X. depelim X.
  - intros.
    rewrite it_mkProd_or_LetIn_app in X.
    simpl in X.
    eapply assumption_context_app in H as [H H'].
    destruct x as [na [b|] ty].
    + elimtype False. inv H'.
    + rewrite /mkProd_or_LetIn /= in X.
      destruct ctx' using rev_ind.
      * simpl in X.
        now eapply ws_cumul_pb_Prod_Sort_inv in X.
      * eapply assumption_context_app in H0 as [H0 Hx].
        destruct x as [na' [b'|] ty']; [elimtype False; inv Hx|].
        rewrite it_mkProd_or_LetIn_app in X.
        rewrite /= /mkProd_or_LetIn /= in X.
        eapply cumul_Prod_Prod_inv in X as [eqann [Hdom Hcodom]]; auto.
        specialize (IHctx (Γ ,, vass na' ty') l0 s s' H H0 Hcodom).
        clear IHctx'.
        intuition auto.
        eapply All2_fold_app.
        ** eapply (All2_fold_length a).
        ** constructor; [constructor|constructor; auto].
        ** unshelve eapply (All2_fold_impl a).
           simpl; intros Γ0 Γ' d d'.
           rewrite !app_context_assoc.
           intros X; destruct X.
           *** constructor; auto.
              eapply conv_conv_ctx; eauto.
              eapply conv_context_app_same.
              constructor; [apply conv_ctx_refl|constructor; auto]; now symmetry.
           *** constructor; auto; eapply conv_conv_ctx; eauto.
              **** eapply conv_context_app_same.
                constructor; [apply conv_ctx_refl|constructor;auto];
                now symmetry.
              **** eapply conv_context_app_same.
                constructor; [apply conv_ctx_refl|constructor;auto];
                now symmetry.
Qed.*)

(** 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. exists (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.

  (* TODO Rename to ws_cumul_pb_Prod_Ind_inv *)

  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.


(*Section ConvCum.
  Import PCUICCumulativity.
  Context {cf : checker_flags}.
  Context (Σ : global_env_ext) (wfΣ : wf Σ).


  Lemma conv_sq_ws_cumul_pb {pb Γ u v} :
    ∥ Σ ;;; Γ |-u = v ∥ -> sq_ws_cumul_pb leq Σ Γ u v.
  Proof.
    intros h; destruct pb.
    - cbn. assumption.
    - destruct h. cbn.
      constructor. now eapply conv_cumul.
  Qed.

  #[global]
  Instance conv_cum_trans {pb Γ} :
    RelationClasses.Transitive (sq_ws_cumul_pb leq Σ Γ).
  Proof.
    intros u v w h1 h2. destruct pb; cbn in *; sq. etransitivity; eassumption.
  Qed.

  *)

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_Case {Γ indn p brs u v} :
    Σ ;;; Γ ⊢ u = v ->
    Σ ;;; Γ ⊢ tCase indn p u brs ≤ tCase indn p v brs.
  Proof.
    intros Γ [ind n] p brs u v h.
    induction h.
    - constructor. constructor; auto.
      + reflexivity.
      + eapply All2_same.
        intros. split ; reflexivity.
    - eapply cumul_red_l ; eauto.
      constructor. assumption.
    - eapply cumul_red_r ; eauto.
      constructor. assumption.
  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 :
    forall Γ 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.


  (*Lemma conv_context_red_context Γ Γ' Δ Δ' :
    ws_cumul_ctx_pb false Σ (Γ ,,, Δ) (Γ' ,,, Δ') ->
    #|Γ| = #|Γ'| ->
    ∑ Δ1 Δ1', red_ctx_rel Σ Γ Δ Δ1 × red_ctx_rel Σ Γ' Δ' Δ1' ×
      eq_context_upto Σ (eq_universe Σ) (eq_universe Σ) Δ1 Δ1'.
  Proof.
    intros.
    pose proof (closed_con)
    pose proof (length_of X). len in H0.
    eapply conv_context_red_context in X as [Δ1 [Δ1' [[redl redr] eq]]]; auto.
    exists (firstn #|Δ| Δ1), (firstn #|Δ'| Δ1').
    have l := (length_of redl). len in l.
    have l' := (length_of redr). len in l'.
    intuition auto.
    - eapply red_ctx_rel_red_context_rel => //.
      rewrite -(firstn_skipn #|Δ| Δ1) in redl.
      eapply All2_fold_app_inv in redl as [].
      * red. eapply All2_fold_impl; tea => /= //.
        intros ???? []; constructor; auto.
      * rewrite firstn_length_le //.
        pose proof (length_of redl).
        rewrite firstn_skipn in H1.
        len in H0. lia.
    - eapply red_ctx_rel_red_context_rel => //.
      rewrite -(firstn_skipn #|Δ'| Δ1') in redr.
      eapply All2_fold_app_inv in redr as [].
      * red. eapply All2_fold_impl; tea => /= //.
        intros ???? []; constructor; auto.
      * rewrite firstn_length_le //. lia.
    - rewrite -(firstn_skipn #|Δ'| Δ1') in eq.
      rewrite -(firstn_skipn #|Δ| Δ1) in eq.
      eapply All2_fold_app_inv in eq as [] => //.
      rewrite !firstn_length_le => //; try lia.
  Qed.*)

  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 OnOne2_conv_open_left {pb Γ x y} :
    All2 (ws_cumul_pb le Σ Γ) x y ->
    forallb (is_open_term Γ) x.
  Proof.
    induction 1; cbn. *)

  Lemma All2_many_OnOne2_pres {A} (R : A -> A -> Type) (P : A -> Type) l l' :
    All2 R l l' ->
    (forall 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.
      exists (tCase ci (set_preturn p v) c brs).
      exists (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.
        exists (tCase ci (set_pparams ppuinst (x1 ++ v :: x2)) c brs).
        exists (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 :
    forall Γ 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 :
    forall 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.
    exists (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 ×
        Σ;;; Γ ,,, fix_context mfix ⊢ dbody u = dbody v ×
        rarg u = rarg v ×
        (eq_binder_annot (dname u) (dname v))
      ) mfix mfix''
    ).
    { set (P1 := fun u v => Σ ;;; Γ ⊢ u = v).
      set (P2 := fun u v => Σ ;;; Γ ,,, fix_context mfix ⊢ u = v).
      change (
        All2 (fun u v =>
          P1 u.(dtype) v.(dtype) ×
          P2 u.(dbody) v.(dbody) ×
          (rarg u = rarg v) *
          (eq_binder_annot (dname u) (dname v))
        ) mfix mfix'
      ) in h.
      change (
        ∑ mfix'',
          All2 (fun u v =>
            P1 u.(dtype) v.(dtype) × dbody u = dbody v × (rarg u = rarg v) ×
            (eq_binder_annot (dname u) (dname v))
          ) mfix'' mfix' ×
          All2 (fun u v =>
            dtype u = dtype v × P2 u.(dbody) v.(dbody) × rarg u = rarg v ×
            (eq_binder_annot (dname u) (dname v))
          ) mfix mfix''
      ).
      clearbody P1 P2. clear opl opr.
      induction h.
      - exists []. repeat split. all: constructor.
      - destruct IHh as [l'' [h1 h2]].
        eexists (mkdef _ (dname x) _ _ _ :: l''). repeat split.
        + constructor. 2: assumption.
          simpl. intuition eauto.
        + constructor. 2: assumption.
          intuition eauto.
    }
    destruct h' as [mfix'' [h1 h2]].
    assert (is_open_mfix Γ mfix'').
    { cbn in opl. eapply forallb_All in opl.
      eapply All2_All_mix_left in h2; tea.
      cbn. rewrite -(All2_length h2). solve_all.
      move: a => /andP[].
      move: a2 => /ws_cumul_pb_is_open_term/and3P[] _.
      rewrite !app_length !fix_context_length => onbody onbody'.
      rewrite /test_def /= a1 => -> /= _.
      rewrite shiftnP_add //. }
    etransitivity.
    - eapply ws_cumul_pb_fix_bodies. 4:tea. all:assumption.
    - eapply ws_cumul_pb_fix_types. all: assumption.
  Qed.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

End ConvRedConv.

(* Lemma untyped_substitution_conv `{cf : checker_flags} (Σ : global_env_ext) Γ Γ' Γ'' s M N :
  wf Σ -> wf_local Σ (Γ ,,, Γ' ,,, Γ'') ->
  untyped_subslet Γ s Γ' ->
  Σ ;;; Γ ,,, Γ' ,,, Γ'' ⊢ M = N ->
  Σ ;;; Γ ,,, subst_context s 0 Γ'' ⊢ subst s #|Γ''| M = subst s #|Γ''| N.
Proof.
  intros wfΓ Hs. induction 1.
  - cbn. now rewrite !subst_empty /= subst0_context.
  - eapply substitution_untyped_let_red in r. 3:eauto. all:eauto with wf.
    eapply red_conv_conv; eauto.
  - eapply substitution_untyped_let_red in r. 3:eauto. all:eauto with wf.
    eapply red_conv_conv_inv; eauto.
Qed. *)

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

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

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

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

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

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

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

  Derive Signature for untyped_subslet.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

End ConvSubst.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

End ConvTerms.

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

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


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

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

Local Open Scope sigma_scope.

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

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

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

End CumulSubst.

Section MoreCongruenceLemmas.

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

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

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

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

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


End MoreCongruenceLemmas.

Section CumulSpecIsCumulAlgo.

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

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

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

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

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

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

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


From MetaCoq.PCUIC Require Import PCUICContextSubst.

Lemma expand_lets_k_app (Γ Γ' : context) t k : expand_lets_k (Γ ++ Γ') k t =
  expand_lets_k Γ' (k + context_assumptions Γ) (expand_lets_k Γ k t).
Proof.
  revert Γ k t.
  induction Γ' as [|[na [b|] ty] Γ'] using ctx_length_rev_ind; intros Γ k t.
  - simpl. now rewrite /expand_lets_k /= subst_empty lift0_id app_nil_r.
  - simpl; rewrite app_assoc !expand_lets_k_vdef /=; len; simpl.
    rewrite subst_context_app. specialize (H (subst_context [b] 0 Γ') ltac:(now len)).
    specialize (H (subst_context [b] #|Γ'| Γ)). rewrite Nat.add_0_r /app_context H; len.
    f_equal.
    rewrite /expand_lets_k; len.
    rewrite -Nat.add_assoc.
    rewrite distr_subst_rec; len.
    epose proof (subst_extended_subst_k [b] Γ #|Γ'| 0).
    rewrite Nat.add_0_r Nat.add_comm in H0. rewrite -H0. f_equal.
    rewrite commut_lift_subst_rec. 1:lia. lia_f_equal.
  - simpl. rewrite app_assoc !expand_lets_k_vass /=; len; simpl.
    now rewrite (H Γ' ltac:(reflexivity)).
Qed.

Lemma expand_lets_app Γ Γ' t : expand_lets (Γ ++ Γ') t =
  expand_lets_k Γ' (context_assumptions Γ) (expand_lets Γ t).
Proof.
  now rewrite /expand_lets expand_lets_k_app.
Qed.

Lemma subst_rel0_lift_id n t : subst [tRel 0] n (lift 1 (S n) t) = t.
Proof using Type.
  rewrite subst_reli_lift_id; try lia.
  now rewrite lift0_id.
Qed.


(****************************)
(* Iterated beta reduction  *)
(****************************)

Section IteratedBetaReduction.
  Context `{cf : checker_flags}.

  Lemma red_betas0 (Σ:global_env_ext) (wfΣ:wf Σ) Γ (Δ : context) l t t' :
    #|l| = context_assumptions Δ ->
    closedn #|Γ,,, Δ| t ->
    closed_ctx (Γ ,,, Δ) ->
    PCUICReduction.red Σ.1 (Γ ,,, Δ) t t' ->
    PCUICReduction.red Σ.1 Γ (mkApps (it_mkLambda_or_LetIn Δ t) l) (subst0 (List.rev l) (expand_lets Δ t')).
  Proof using cf.
    elim: Δ t t' l=> [|[na[a|]ty] ls ih] /= t t' l.
    - move=> /length_nil -> * /=.
      rewrite PCUICLiftSubst.subst_empty PCUICSigmaCalculus.expand_lets_nil //.
    - move=> /ih ih0 clt clctx red. rewrite -/([_] ++ _).
      move: (clctx); rewrite Nat.add_0_r => /andP [clctx0 cld].
      rewrite expand_lets_app /= -/(expand_lets ls).
      refine (ih0 _ _ _ _ _)=> //.
      1: apply: PCUICClosed.closedn_mkLambda_or_LetIn=> //.
      rewrite /mkLambda_or_LetIn /= /expand_lets /expand_lets_k /=.
      rewrite PCUICLiftSubst.subst_empty PCUICLiftSubst.lift0_p.
      apply: PCUICReduction.red_step; first exact: PCUICReduction.red_zeta.
      rewrite PCUICLiftSubst.lift0_id.
      refine (substitution_untyped_red (Σ:=Σ) (Γ := Γ,,, ls) (Δ := [_]) (Γ':=nil) (M := t) (N:=t') _ _ _ red).
      + apply: untyped_subslet_def_tip=> //.
      + rewrite -PCUICClosedTyp.is_open_term_closed //.
      + rewrite on_free_vars_ctx_on_ctx_free_vars -PCUICClosedTyp.is_closed_ctx_closed //.
    - move: l=> /snocP [//|/=l x].
      rewrite app_length /= Nat.add_comm PCUICAstUtils.mkApps_app /= => [=] eq.
      move: (eq)=> /ih ih0 clt clctx red.
      move: (clctx); rewrite Nat.add_0_r => /andP [clctx0 cld].
      etransitivity.
      1:{
        apply: PCUICReduction.red_app; last reflexivity.
        apply: ih0.
        + apply: PCUICClosed.closedn_mkLambda_or_LetIn=> //.
        + assumption.
        + apply: red_abs_alt; first reflexivity; eassumption.
      }
      apply: PCUICReduction.red_step=> /=; first apply: PCUICReduction.red_beta.
      set t0 := (t in PCUICReduction.red _ _ t _).
      set t1 := (t in PCUICReduction.red _ _ _ t).
      have -> // : t0 = t1.
      rewrite {}/t0 {}/t1.
      rewrite /subst1 -PCUICLiftSubst.subst_app_simpl -(rev_app_distr _ [x]).
      f_equal; rewrite -/([_]++ls) expand_lets_app /= /expand_lets.
      rewrite {-1}/expand_lets_k /=subst_rel0_lift_id //.
  Qed.

  Lemma red_betas (Σ:global_env_ext) (wfΣ:wf Σ) Γ (Δ : context) l t :
    #|l| = context_assumptions Δ ->
    closedn #|Γ,,, Δ| t ->
    closed_ctx (Γ ,,, Δ) ->
    PCUICReduction.red Σ.1 Γ (mkApps (it_mkLambda_or_LetIn Δ t) l) (subst0 (mk_ctx_subst Δ l) t).
  Proof using cf.
    move=> eql.
    move: (mk_ctx_subst_spec (eq_sym eql))=> /(context_subst_subst_expand_lets _ _ _ t 0) ->.
    move=> *; apply: red_betas0=> //.
  Qed.

  Lemma red_betas_typed (Σ:global_env_ext) (wfΣ:wf Σ) Γ (Δ : context) l t T :
    #|l| = context_assumptions Δ ->
    Σ ;;; Γ ,,, Δ |- t : T ->
    PCUICReduction.red Σ.1 Γ (mkApps (it_mkLambda_or_LetIn Δ t) l) (subst0 (mk_ctx_subst Δ l) t).
  Proof using cf.
    move=> eql ty; apply: red_betas=> //.
    1: apply: PCUICClosedTyp.subject_closed; eassumption.
    apply: PCUICClosedTyp.closed_wf_local; apply: typing_wf_local; eassumption.
  Qed.

  Lemma conv_betas (Σ : global_env_ext) (wfΣ: wf Σ) Γ Δ l t :
    closedn #|Γ ,,, Δ| t ->
    closed_ctx (Γ ,,, Δ) ->
    forallb (closedn #|Γ|) l ->
    context_assumptions Δ = #|l|  ->
    Σ ;;; Γ |- mkApps (it_mkLambda_or_LetIn Δ t) l =s subst0 (mk_ctx_subst Δ l) t.
  Proof using cf.
    move=> tws /[dup] ?.
    rewrite PCUICClosed.closedn_ctx_app=> /andP[??] lcl eqlen.
    apply: cumulAlgo_cumulSpec.
    apply PCUICContextConversion.ws_cumul_pb_red.
    set (u:= mkApps _ _).
    set (w := subst0 _ _).
    exists w, w; split; last reflexivity.
    + constructor.
      * by rewrite  -PCUICClosedTyp.is_closed_ctx_closed.
      * rewrite /u -PCUICClosedTyp.is_open_term_closed PCUICClosed.closedn_mkApps lcl andb_true_r.
        apply: PCUICClosed.closedn_it_mkLambda_or_LetIn => //.
        by rewrite Nat.add_comm -app_length.
      * apply: red_betas=> //.
    + constructor.
      * by rewrite  -PCUICClosedTyp.is_closed_ctx_closed.
      * rewrite -PCUICClosedTyp.is_open_term_closed.
        move: (eqlen)=> /mk_ctx_subst_spec /closedn_ctx_subst_forall h.
        apply: PCUICClosed.closedn_subst0; first by apply: h.
        rewrite mk_ctx_subst_length //.
        by rewrite Nat.add_comm -app_length.
      * reflexivity.
  Qed.

End IteratedBetaReduction.
