Library MetaCoq.PCUIC.PCUICSR

From MetaCoq.Template Require Import config utils.
From MetaCoq.PCUIC Require Import PCUICAst PCUICAstUtils PCUICTactics PCUICUtils PCUICOnOne
     PCUICLiftSubst PCUICUnivSubst PCUICTyping PCUICGlobalEnv PCUICWeakeningEnvConv
     PCUICWeakeningEnvTyp PCUICWeakeningConv PCUICWeakeningTyp
     PCUICSubstitution PCUICCasesContexts PCUICClosed PCUICClosedTyp PCUICClosedConv
     PCUICCumulativity PCUICGeneration PCUICReduction
     PCUICAlpha PCUICEquality PCUICValidity PCUICParallelReductionConfluence
     PCUICConfluence PCUICContextConversion PCUICContextConversionTyp
     PCUICUnivSubstitutionConv PCUICUnivSubstitutionTyp
     PCUICConversion PCUICInversion PCUICContexts PCUICArities
     PCUICWellScopedCumulativity PCUICGuardCondition
     PCUICParallelReduction PCUICSpine PCUICInductives PCUICInductiveInversion PCUICSigmaCalculus.

Require Import ssreflect ssrbool Utf8.
From Equations Require Import Equations.
From Equations.Type Require Import Relation Relation_Properties.
Require Import Equations.Prop.DepElim.
Local Set SimplIsCbn.

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

Derive Signature for OnOne2_local_env.

Ltac rename_hyp h ht ::= my_rename_hyp h ht.

Arguments Nat.sub : simpl nomatch.
Arguments Universe.sort_of_product : simpl nomatch.


Lemma wf_fixpoint_red1_type {cf Σ} {wfΣ : wf Σ} Γ mfix mfix1 :
  wf_fixpoint Σ mfix
  OnOne2
  (fun x y : def term
   closed_red1 Σ Γ (dtype x) (dtype y)
   × (dname x, dbody x, rarg x) = (dname y, dbody y, rarg y)) mfix mfix1
  wf_fixpoint Σ mfix1.
Proof.
  intros wffix o.
  move: wffix; unfold wf_fixpoint, wf_fixpoint_gen.
  move/andb_and ⇒ [] isl wf. apply/andP; split.
  { clear wf. solve_all.
    revert isl.
    induction o; depelim isl; constructor; auto. destruct p.
    destruct c. noconf e. congruence. }
  clear isl. move: wf.
  enough ( inds, map_option_out (map check_one_fix mfix) = Some inds
     map_option_out (map check_one_fix mfix1) = Some inds) ⇒ //.
  destruct map_option_out. now specialize (H _ eq_refl) as →.
  discriminate.
  induction o; intros inds.
  - simpl.
    destruct p as [redty eqs].
    destruct hd as [dname dtype dbody rarg], hd' as [dname' dtype' dbody' rarg'].
    simpl in ×.
    noconf eqs.
    destruct (decompose_prod_assum [] dtype) eqn:decomp.
    destruct nth_error eqn:Hnth.
    apply decompose_prod_assum_it_mkProd_or_LetIn in decomp.
    simpl in decomp.
    subst dtype.
    destruct (red1_it_mkProd_or_LetIn_smash redty Hnth) as
      (ctx & t' & decomp & d & [hnth di]).
    rewrite decomp hnth.
    unfold head in di. destruct decompose_app; simpl in ×.
    destruct destInd as [[ind u]|]; try discriminate.
    destruct decompose_app. simpl in di. rewrite di. auto.
    discriminate.
  - simpl map.
    simpl map_option_out.
    destruct check_one_fix ⇒ //.
    destruct map_option_out. specialize (IHo _ eq_refl).
    move⇒ [= <-]. now rewrite IHo.
    discriminate.
Qed.

Lemma wf_fixpoint_red1_body {cf Σ} {wfΣ : wf Σ} Γ mfix mfix1 :
  wf_fixpoint Σ mfix
  OnOne2
  (fun x y : def term
   closed_red1 Σ Γ (dbody x) (dbody y)
   × (dname x, dtype x, rarg x) = (dname y, dtype y, rarg y)) mfix mfix1
  wf_fixpoint Σ mfix1.
Proof.
  intros wffix o.
  move: wffix; unfold wf_fixpoint, wf_fixpoint_gen.
  move/andb_and ⇒ [] isl wf. apply/andP; split.
  { clear wf. solve_all.
    revert isl.
    induction o; depelim isl; constructor; auto. destruct p.
    destruct c. noconf e.
    destruct (dbody hd) ⇒ //. depelim clrel_rel; solve_discr.
    now rewrite H. now rewrite H. }
  clear isl. move: wf.
  enough (map check_one_fix mfix = map check_one_fix mfix1) as → ⇒ //.
  induction o.
  - simpl. f_equal.
    destruct p as [redty eqs].
    destruct hd as [dname dtype dbody rarg], hd' as [dname' dtype' dbody' rarg'].
    simpl in ×.
    noconf eqs. reflexivity.
  - simpl. now rewrite IHo.
Qed.

Lemma wf_cofixpoint_red1_type {cf:checker_flags} (Σ : global_env_ext) Γ mfix mfix1 :
  wf Σ.1
  wf_cofixpoint Σ.1 mfix
  OnOne2
  (fun x y : def term
   Σ ;;; Γ dtype x dtype y
   × (dname x, dbody x, rarg x) = (dname y, dbody y, rarg y)) mfix mfix1
  wf_cofixpoint Σ.1 mfix1.
Proof.
  intros wfΣ wffix o.
  move: wffix; unfold wf_cofixpoint, wf_cofixpoint_gen.
  enough ( inds, map_option_out (map check_one_cofix mfix) = Some inds
     map_option_out (map check_one_cofix mfix1) = Some inds) ⇒ //.
  destruct map_option_out. now specialize (H _ eq_refl) as →.
  discriminate.
  induction o; intros inds.
  - simpl.
    destruct p as [redty eqs].
    destruct hd as [dname dtype dbody rarg], hd' as [dname' dtype' dbody' rarg'].
    simpl in ×.
    noconf eqs.
    destruct (decompose_prod_assum [] dtype) eqn:decomp.
    apply decompose_prod_assum_it_mkProd_or_LetIn in decomp.
    simpl in decomp.
    subst dtype.
    destruct (decompose_app t) as [f l] eqn:decomp.
    destruct f; try discriminate. simpl.
    apply decompose_app_inv in decomp. subst t.
    eapply red_it_mkProd_or_LetIn_mkApps_Ind in redty as [ctx' [args' ->]]; auto.
    erewrite decompose_prod_assum_it_mkProd ⇒ //.
    2:{ now rewrite is_ind_app_head_mkApps. }
    rewrite decompose_app_mkApps ⇒ //.
  - simpl map.
    simpl map_option_out.
    destruct check_one_cofix ⇒ //.
    destruct map_option_out. specialize (IHo _ eq_refl).
    move⇒ [= <-]. now rewrite IHo.
    discriminate.
Qed.

Lemma wf_cofixpoint_red1_body {cf:checker_flags} (Σ : global_env_ext) Γ mfix mfix1 :
  wf Σ.1
  wf_cofixpoint Σ.1 mfix
  OnOne2
  (fun x y : def term
   red1 Σ Γ (dbody x) (dbody y)
   × (dname x, dtype x, rarg x) = (dname y, dtype y, rarg y)) mfix mfix1
  wf_cofixpoint Σ.1 mfix1.
Proof.
  intros wfΣ wffix o.
  move: wffix; unfold wf_cofixpoint, wf_cofixpoint_gen.
  enough (map check_one_cofix mfix = map check_one_cofix mfix1) as → ⇒ //.
  induction o.
  - simpl. f_equal.
    destruct p as [redty eqs].
    destruct hd as [dname dtype dbody rarg], hd' as [dname' dtype' dbody' rarg'].
    simpl in ×.
    noconf eqs. reflexivity.
  - simpl. now rewrite IHo.
Qed.

#[global] Hint Extern 0 (conv_decls _ _ _ _ _) ⇒ constructor : pcuic.
#[global] Hint Extern 0 (cumul_decls _ _ _ _ _) ⇒ constructor : pcuic.
#[global] Hint Extern 0 (conv_context _ _ _) ⇒ constructor : pcuic.
#[global] Hint Extern 0 (cumul_context _ _ _) ⇒ constructor : pcuic.

#[global] Hint Extern 4 ( s : Universe.t, typing _ _ ?T (tSort s)) ⇒
  match goal with
  | [ H : isType _ _ T |- _ ] ⇒ exact H
  end : pcuic.

Ltac unfold_pcuic :=
  progress (unfold PCUICTypingDef.typing, PCUICLookup.wf_universe in × ).
#[global] Hint Extern 10 ⇒ unfold_pcuic : pcuic.

#[global] Hint Resolve red_conv red1_red red_cumul : pcuic.
#[global] Hint Transparent global_env_ext : pcuic.
#[global] Hint Constructors All_local_env : pcuic.
Ltac pcuics := try typeclasses eauto with pcuic.

Lemma declared_projection_declared_constructor {cf}
  {Σ} {wfΣ : wf Σ} {p mdecl mdecl' idecl idecl' pdecl cdecl cdecl'} :
  declared_projection Σ p mdecl idecl cdecl pdecl
  declared_constructor Σ (p.(proj_ind), 0) mdecl' idecl' cdecl'
  mdecl = mdecl' idecl = idecl' cdecl = cdecl'.
Proof.
  intros [[] ?] [].
  pose proof (declared_inductive_inj H H2). intuition auto. subst.
  rewrite H0 in H3. congruence.
Qed.

Ltac hide H :=
  match type of H with
  | ?tychange ty with (@hidebody _ ty) in H
  end.

Lemma All2i_nth_error {A B} {P : nat A B Type} {l l' n x c k} :
  All2i P k l l'
  nth_error l n = Some x
  nth_error l' n = Some c
  P (k + n)%nat x c.
Proof.
  induction 1 in n |- ×.
  × rewrite !nth_error_nil ⇒ //.
  × destruct n.
    + simpl. intros [= <-] [= <-]. now rewrite Nat.add_0_r.
    + simpl. intros hnth hnth'. specialize (IHX _ hnth hnth').
      now rewrite Nat.add_succ_r.
Qed.

Lemma conv_context_smash_end {cf Σ} {wfΣ : wf Σ} (Γ Δ Δ' : context) :
  wf_local Σ (Γ ,,, Δ)
  wf_local Σ (Γ ,,, Δ')
  Σ Γ ,,, Δ = Γ ,,, Δ'
  Σ Γ ,,, smash_context [] Δ = Γ ,,, smash_context [] Δ'.
Proof.
  intros wf wf' cv.
  eapply ws_cumul_ctx_pb_rel_app.
  apply ws_cumul_ctx_pb_rel_app in cv.
  eapply ws_cumul_ctx_pb_rel_smash ⇒ //.
Qed.

Lemma expand_lets_eq Γ t :
  expand_lets Γ t =
  subst0 (extended_subst Γ 0) (lift (context_assumptions Γ) #|Γ| t).
Proof.
  rewrite /expand_lets /expand_lets_k /= //.
Qed.

Lemma expand_lets_eq_map Γ l :
  map (expand_lets Γ) l =
  map (subst0 (extended_subst Γ 0)) (map (lift (context_assumptions Γ) #|Γ|) l).
Proof.
  rewrite /expand_lets /expand_lets_k /= map_map_compose //.
Qed.

Lemma map_expand_lets_to_extended_list Γ :
  map (expand_lets Γ) (to_extended_list Γ) = to_extended_list (smash_context [] Γ).
Proof.
  now rewrite expand_lets_eq_map map_subst_extended_subst_lift_to_extended_list_k.
Qed.

Lemma conv_context_rel_reln {cf} {Σ} {le} Γ Δ Δ' :
  ws_cumul_ctx_pb_rel le Σ Γ Δ Δ'
   acc n, reln acc n Δ = reln acc n Δ'.
Proof.
  intros [cl a]. induction a.
  - constructor.
  - intros acc n; destruct p; simpl; auto.
Qed.

Lemma conv_context_rel_to_extended_list {cf} {Σ} {le} {Γ Δ Δ'} :
  ws_cumul_ctx_pb_rel le Σ Γ Δ Δ'
  to_extended_list Δ = to_extended_list Δ'.
Proof.
  unfold to_extended_list, to_extended_list_k.
  intros; now eapply conv_context_rel_reln.
Qed.

Require Import PCUICOnFreeVars.

Lemma eq_context_alpha_conv {cf} {Σ} {wfΣ : wf Σ} Γ Δ Δ' :
  eq_context_upto_names Δ Δ'
  is_closed_context (Γ ,,, Δ)
  is_closed_context (Γ ,,, Δ')
  ws_cumul_ctx_pb_rel Conv Σ Γ Δ Δ'.
Proof.
  induction 1.
  - constructor; auto. constructor.
  - rewrite /= !on_free_vars_ctx_snoc ⇒ /andP[] cl;
    generalize cl; rewrite on_free_vars_ctx_app ⇒ /andP[] clΓ cll clx /andP[] clΓ' cly.
    intros; destruct r; constructor ⇒ //.
    × constructor. apply IHX ⇒ //. constructor; auto; subst.
      cbn in clx, cly.
      eapply into_ws_cumul_pb; eauto.
    × constructor. apply IHX ⇒ //.
      move/andP: clx ⇒ /= [clb clty].
      move/andP: cly ⇒ /= [clb' clty'].
      constructor; auto; subst.
      eapply into_ws_cumul_pb; eauto.
      eapply into_ws_cumul_pb; eauto.
Qed.

Lemma eq_context_alpha_reln Δ Δ' :
  eq_context_upto_names Δ Δ'
   acc n, reln acc n Δ = reln acc n Δ'.
Proof.
  induction 1.
  - constructor.
  - intros acc n; destruct r; simpl; auto.
Qed.

Lemma eq_context_alpha_to_extended_list Δ Δ' :
  eq_context_upto_names Δ Δ'
  to_extended_list Δ = to_extended_list Δ'.
Proof.
  unfold to_extended_list, to_extended_list_k.
  intros; now eapply eq_context_alpha_reln.
Qed.

Lemma reln_set_binder_name brctx Γ :
  All2 (fun (x : binder_annot name) (y : context_decl) ⇒
    eq_binder_annot x (decl_name y)) brctx Γ
   acc n, reln acc n (map2 set_binder_name brctx Γ) = reln acc n Γ.
Proof.
  move/All2_lengthhl.
  induction brctx in Γ, hl |- *; destruct Γ as [|hd tl]; simpl in hl |- *; try congruence.
  intros acc n.
  destruct hd as [na [b|] ty]; cbn; apply IHbrctx; congruence.
Qed.

Lemma to_extended_list_set_binder_name brctx Γ :
  All2 (fun (x : binder_annot name) (y : context_decl) ⇒
    eq_binder_annot x (decl_name y)) brctx Γ
  to_extended_list_k (map2 set_binder_name brctx Γ) =1 to_extended_list_k Γ.
Proof.
  now intros hl x; eapply reln_set_binder_name.
Qed.

Lemma to_extended_list_case_branch_context ci mdecl p brctx cdecl :
  All2 (fun x yeq_binder_annot x y.(decl_name)) brctx (cstr_args cdecl)
  to_extended_list (case_branch_context ci mdecl p brctx cdecl) =
  to_extended_list (cstr_args cdecl).
Proof.
  intros hlen.
  rewrite /to_extended_list /case_branch_context /case_branch_context_gen.
  rewrite /pre_case_branch_context_gen /inst_case_context /cstr_branch_context.
  rewrite to_extended_list_set_binder_name //; try by
  rewrite to_extended_list_k_subst /expand_lets_ctx /expand_lets_k_ctx; substu;
  rewrite to_extended_list_k_subst
    to_extended_list_k_lift_context to_extended_list_k_subst
    PCUICLiftSubst.map_subst_instance_to_extended_list_k //.
  induction hlen; cbn. constructor.
  rewrite subst_context_snoc /= expand_lets_ctx_snoc subst_context_snoc.
  constructor. now cbn. apply IHhlen.
Qed.

Lemma spine_subst_inst_subst {cf} {Σ} {Γ inst s Δ Δ'} :
  spine_subst Σ Γ inst s Δ
  subst_context s 0 Δ' = subst_context (List.rev inst) 0 (expand_lets_ctx Δ Δ').
Proof.
  intros sp. pose proof (spine_subst_subst_to_extended_list_k sp).
  rewrite -H.
  rewrite /expand_lets_ctx /expand_lets_k_ctx /=.
  rewrite -map_rev.
  rewrite subst_context_subst_context. len.
  rewrite subst_context_lift_context_cancel. now len.
  f_equal.
  rewrite map_rev. rewrite H.
  apply context_subst_subst_extended_subst. apply sp.
Qed.

Lemma spine_subst_inst_subst_term {cf} {Σ} {Γ inst s Δ Δ'} :
  spine_subst Σ Γ inst s Δ
  subst s 0 Δ' = subst (List.rev inst) 0 (expand_lets Δ Δ').
Proof.
  intros sp. pose proof (spine_subst_subst_to_extended_list_k sp).
  rewrite -H.
  rewrite /expand_lets_ctx /expand_lets_k_ctx /=.
  rewrite -map_rev.
  rewrite distr_subst. len.
  rewrite simpl_subst_k. now len.
  f_equal.
  rewrite map_rev. rewrite H.
  apply context_subst_subst_extended_subst. apply sp.
Qed.

Lemma subst_context_subst_context s k s' Γ :
  subst_context s k (subst_context s' k Γ) =
  subst_context (map (subst0 s) s') k (subst_context s (k + #|s'|) Γ).
Proof.
  induction Γ as [|[na [b|] ty] Γ']; simpl; auto;
    rewrite !subst_context_snoc /= /subst_decl /map_decl /=; f_equal;
    auto; f_equal; len;
  rewrite -{1}(Nat.add_0_r (#|Γ'| + k)) distr_subst_rec; lia_f_equal.
Qed.

Lemma spine_subst_inst_subst_k {cf} {Σ} {Γ inst s Δ k Δ'} :
  spine_subst Σ Γ inst s Δ
  subst_context s k Δ' = subst_context (List.rev inst) k (expand_lets_k_ctx Δ k Δ').
Proof.
  intros sp. pose proof (spine_subst_subst_to_extended_list_k sp).
  rewrite -H.
  rewrite /expand_lets_ctx /expand_lets_k_ctx /=.
  rewrite -map_rev.
  rewrite subst_context_subst_context. len.
  rewrite subst_context_lift_context_cancel. now len.
  f_equal.
  rewrite map_rev. rewrite H.
  apply context_subst_subst_extended_subst. apply sp.
Qed.

Lemma spine_subst_inst_subst_term_k {cf} {Σ} {Γ inst s Δ k Δ'} :
  spine_subst Σ Γ inst s Δ
  subst s k Δ' = subst (List.rev inst) k (expand_lets_k Δ k Δ').
Proof.
  intros sp. pose proof (spine_subst_subst_to_extended_list_k sp).
  rewrite -H.
  rewrite /expand_lets_ctx /expand_lets_k_ctx /=.
  rewrite -map_rev /expand_lets_k.
  rewrite -{2}(Nat.add_0_r k) distr_subst_rec. len.
  rewrite simpl_subst_k. now len.
  f_equal.
  rewrite map_rev. rewrite H.
  apply context_subst_subst_extended_subst. apply sp.
Qed.

Lemma isType_weaken {cf} {Σ Γ Δ T} {wfΣ : wf Σ} :
  wf_local Σ Δ
  isType Σ Γ T
  isType Σ (Δ ,,, Γ) T.
Proof.
  intros wfΔ HT.
  apply infer_typing_sort_impl with id HT; intros Hs.
  eapply weaken_ctx ⇒ //.
Qed.

The crucial property on constructors of cumulative inductive types for type preservation: we don't need to compare their instances when fully applied.
Lemma R_global_instance_cstr_irrelevant {cf} {Σ} {wfΣ : wf Σ} {ci c} {mdecl idecl cdecl u u'} :
  declared_constructor Σ (ci, c) mdecl idecl cdecl
  R_ind_universes Σ ci (context_assumptions (ind_params mdecl) + #|cstr_indices cdecl|) u u'
  R_global_instance Σ.1 (eq_universe Σ) (eq_universe Σ) (ConstructRef ci c)
    (ind_npars mdecl + context_assumptions (cstr_args cdecl)) u u'.
Proof.
  intros declc.
  pose proof (on_declared_constructor declc).
  pose proof (on_declared_constructor declc) as [[onind oib] [ctor_sorts [hnth onc]]].
  intros Hu. pose proof (R_global_instance_length _ _ _ _ _ _ _ Hu).
  rewrite /R_global_instance /R_opt_variance /= /lookup_constructor.
  rewrite (declared_inductive_lookup declc) (proj2 declc).
  rewrite -(cstr_args_length onc).
  case: leb_spec_Set; try lia. move_ /=; cbn.
  now apply R_universe_instance_variance_irrelevant.
Qed.

Lemma wf_pre_case_branch_context {cf} {Σ} {wfΣ : wf Σ} {Γ ci mdecl idecl p} {br : branch term} {cdecl} :
  declared_inductive Σ ci mdecl idecl
  wf_branch_gen cdecl (forget_types (bcontext br))
  consistent_instance_ext Σ (ind_universes mdecl) (puinst p)
  wf_local Σ (Γ,,, case_branch_context ci mdecl p (forget_types (bcontext br)) cdecl)
  wf_local Σ (Γ,,, pre_case_branch_context ci mdecl (pparams p) (puinst p) cdecl).
Proof.
  movedecli wfbr cu wf.
  eapply wf_local_alpha; tea.
  eapply All2_app. 2:eapply All2_refl; reflexivity.
  eapply All2_symP. tc.
  rewrite /case_branch_context_gen.
  eapply pre_case_branch_context_eq; eauto.
Qed.

Lemma conv_refl' {cf} {Σ} {wfΣ : wf Σ} {Γ x y} :
  x = y
  Σ ;;; Γ |- x = y.
Proof. now intros →. Qed.

Lemma expand_lets_lift_cancel Γ x :
  expand_lets Γ (lift0 #|Γ| x) = lift0 (context_assumptions Γ) x.
Proof.
  rewrite /expand_lets /expand_lets_k.
  simpl. rewrite simpl_lift; try lia.
  rewrite Nat.add_comm.
  rewrite -(simpl_lift _ _ _ _ 0); try lia.
  rewrite simpl_subst_k //. now len.
Qed.

Lemma context_assumptions_expand_lets_k_ctx {Γ k Δ} :
  context_assumptions (expand_lets_k_ctx Γ k Δ) = context_assumptions Δ.
Proof.
  now rewrite /expand_lets_k_ctx; len.
Qed.
#[global]
Hint Rewrite @context_assumptions_expand_lets_k_ctx : len.

Lemma closedn_expand_lets (k : nat) (Γ : context) (t : term) :
  closedn_ctx k Γ
  closedn (k + #|Γ|) t
  closedn (k + context_assumptions Γ) (expand_lets Γ t).
Proof.
  rewrite /expand_lets /expand_lets_k.
  intros clΓ cl.
  eapply closedn_subst0.
  eapply (closedn_extended_subst_gen _ _ 0) ⇒ //.
  len.
  rewrite Nat.add_comm Nat.add_assoc. eapply closedn_lift.
  now rewrite Nat.add_comm.
Qed.

Lemma smash_context_subst_context_let_expand s Γ Δ :
  smash_context [] (subst_context_let_expand s Γ Δ) =
  subst_context_let_expand s Γ (smash_context [] Δ).
Proof.
  rewrite /subst_context_let_expand.
  rewrite (smash_context_subst []).
  now rewrite /expand_lets_ctx /expand_lets_k_ctx (smash_context_subst [])
    (smash_context_lift []).
Qed.

Lemma on_constructor_wf_args {cf} {Σ} {wfΣ : wf Σ} {ind c mdecl idecl cdecl u} :
  declared_constructor Σ (ind, c) mdecl idecl cdecl
  consistent_instance_ext Σ (ind_universes mdecl) u
  wf_local Σ (subst_instance u (ind_params mdecl) ,,,
    (subst_context (ind_subst mdecl ind u)) #|ind_params mdecl| (subst_instance u (cstr_args cdecl))).
Proof.
  intros decl cu.
  pose proof (on_constructor_inst decl _ cu) as [wf _].
  rewrite !subst_instance_app_ctx in wf.
  rewrite -app_context_assoc -(app_context_nil_l (_ ,,, _)) app_context_assoc in wf.
  eapply substitution_wf_local in wf; tea.
  2:eapply (subslet_inds decl cu).
  rewrite app_context_nil_l subst_context_app closed_ctx_subst in wf.
  rewrite closedn_subst_instance_context.
  eapply (declared_inductive_closed_params decl).
  now simpl in wf; len in wf.
Qed.

#[global]
Instance conv_context_refl {cf} Σ {wfΣ : wf Σ} : CRelationClasses.Reflexive (All2_fold (conv_decls cumulAlgo_gen Σ)).
Proof.
  intros x. reflexivity.
Qed.


Lemma on_free_vars_ctx_set_binder_name P Γ nas :
  All2 (fun x yeq_binder_annot x y.(decl_name)) nas Γ
  on_free_vars_ctx P (map2 set_binder_name nas Γ) = on_free_vars_ctx P Γ.
Proof.
  induction 1.
  - simpl; auto.
  - cbn [map2]; rewrite !on_free_vars_ctx_snoc IHX; bool_congr.
    rewrite map2_length. apply (All2_length X).
    rewrite (All2_length X).
    destruct y as [na [b|] ty]; cbn; auto.
Qed.

Lemma is_closed_context_set_binder_name Γ Δ nas :
  All2 (fun x yeq_binder_annot x y.(decl_name)) nas Δ
  is_closed_context (Γ ,,, map2 set_binder_name nas Δ) = is_closed_context (Γ ,,, Δ).
Proof.
  induction 1 in Γ |- ×. cbn; auto.
  rewrite !on_free_vars_ctx_app.
  cbn [map2]. rewrite !on_free_vars_ctx_snoc /=.
  specialize (IHX Γ).
  rewrite !on_free_vars_ctx_app in IHX.
  rewrite andb_assoc IHX -andb_assoc. bool_congr. bool_congr.
  rewrite map2_length; eauto using All2_length.
  rewrite (All2_length X).
  destruct y as [na [bod|] ty]; cbn; auto.
Qed.

Lemma conv_ctx_set_binder_name {cf} {Σ : global_env_ext} {wfΣ : wf Σ} (Γ Δ Δ' : context) (nas : list aname) :
  All2 (fun x yeq_binder_annot x y.(decl_name)) nas Δ
  All2 (fun x yeq_binder_annot x y.(decl_name)) nas Δ'
  ws_cumul_ctx_pb_rel Conv Σ Γ Δ Δ'
  ws_cumul_ctx_pb_rel Conv Σ Γ (map2 set_binder_name nas Δ) (map2 set_binder_name nas Δ').
Proof.
  induction 1 in Δ' |- *; intros H; depelim H; intros [cl H']; split; auto;
  depelim H'. cbn. constructor; auto. eapply IHX; auto. split; auto.
  have clΓl' : is_closed_context (Γ ,,, l').
  { depelim a; cbn in *; now apply ws_cumul_pb_is_closed_context in eqt. }
  have eqctx : Σ Γ,,, map2 set_binder_name l l' = Γ,,, l'.
  { eapply eq_context_upto_ws_cumul_ctx_pb ⇒ //.
    rewrite is_closed_context_set_binder_name //.
    apply eq_context_upto_cat. reflexivity.
    apply eq_context_gen_eq_context_upto; tc.
    apply eq_binder_annots_eq_context_gen_ctx ⇒ //. }
  depelim a; cbn in *; constructor; auto;
  eapply (ws_cumul_pb_ws_cumul_ctx (pb':=Conv)); tea.
Qed.

Lemma OnOne2_All2_All2 {A B : Type} {l1 l2 : list A} {l3 : list B} {R1 : A A Type} {R2 R3 : A B Type} :
  OnOne2 R1 l1 l2
  All2 R2 l1 l3
  ( x y, R2 x y R3 x y)
  ( x y z, R1 x y R2 x z R3 y z)
  All2 R3 l2 l3.
Proof.
  intros o. induction o in l3 |- ×.
  intros H; depelim H.
  intros Hf Hf'. specialize (Hf' _ _ _ p r). constructor; auto.
  eapply All2_impl; eauto.
  intros H; depelim H.
  intros Hf. specialize (IHo _ H Hf).
  constructor; auto.
Qed.

Lemma OnOne2_All2i_All2i {A B : Type} {l1 l2 : list A} {l3 : list B} {R1 : A A Type}
  {R2 R3 : nat B A Type} {n} :
  OnOne2 R1 l1 l2
  All2i R2 n l3 l1
  ( n x y, R2 n x y R3 n x y)
  ( n x y z, R1 x y R2 n z x R3 n z y)
  All2i R3 n l3 l2.
Proof.
  intros o. induction o in n, l3 |- ×.
  intros H; depelim H.
  intros Hf Hf'. specialize (Hf' _ _ _ _ p r0). constructor; auto.
  eapply All2i_impl; eauto.
  intros H; depelim H.
  intros Hf. specialize (IHo _ _ H Hf).
  constructor; auto.
Qed.



Lemma OnOne2_local_env_forget_types P ctx ctx' :
  OnOne2_local_env (on_one_decl P) ctx ctx'
  forget_types ctx = forget_types ctx'.
Proof.
  induction 1; simpl.
  - depelim p; subst; auto.
  - depelim p; subst; auto.
  - f_equal; auto.
Qed.

From MetaCoq.PCUIC Require Import PCUICContextReduction PCUICOnFreeVars.


Lemma red_one_decl_red_ctx {cf} {Σ} {wfΣ : wf Σ} {Γ Δ Δ'} :
  is_closed_context (Γ ,,, Δ)
  OnOne2_local_env (on_one_decl (fun Δ : contextred1 Σ (Γ ,,, Δ))) Δ Δ'
  red_ctx Σ (Γ ,,, Δ) (Γ ,,, Δ').
Proof.
  intros iscl o.
  eapply red_ctx_red_context.
  apply red_context_app.
  eapply red_context_refl.
  apply red_ctx_rel_red_context_rel. tea.
  now apply on_free_vars_ctx_on_ctx_free_vars_closedP_impl.
  constructor. exact o.
Qed.

Lemma into_closed_red_ctx {cf} {Σ} {wfΣ : wf Σ} {Γ Δ} :
  is_closed_context Γ
  red_ctx Σ Γ Δ
  closed_red_ctx Σ Γ Δ.
Proof.
  intros iscl red.
  apply on_free_vars_ctx_All_fold in iscl.
  eapply All2_fold_All_fold_mix_left in red; tea. cbn in red. clear iscl.
  eapply All2_fold_impl_ind ; tea.
  intros ???? IH IH' [wf ad].
  eapply All_decls_on_free_vars_impl; tea.
  intros t t' clt redt.
  eapply into_closed_red; tea.
  eapply All2_fold_prod_inv in IH as [IH _].
  eapply All2_fold_All_left in IH.
  now eapply on_free_vars_ctx_All_fold in IH.
Qed.

Lemma red_one_decl_red_context {cf} {Σ} {wfΣ : wf Σ} {Γ Δ Δ'} :
  is_closed_context (Γ ,,, Δ)
  OnOne2_local_env (on_one_decl (fun Δ : contextred1 Σ (Γ ,,, Δ))) Δ Δ'
  Σ Γ ,,, Δ Γ ,,, Δ'.
Proof.
  intros iscl o.
  eapply into_closed_red_ctx ⇒ //.
  now apply red_one_decl_red_ctx.
Qed.

Lemma red_one_decl_ws_cumul_ctx_pb {cf} {Σ} {wfΣ : wf Σ} {Γ Δ Δ'} :
  is_closed_context (Γ ,,, Δ)
  OnOne2_local_env (on_one_decl (fun Δ : contextred1 Σ (Γ ,,, Δ))) Δ Δ'
  Σ Γ ,,, Δ = Γ ,,, Δ'.
Proof.
  intros; now eapply red_ctx_ws_cumul_ctx_pb, red_one_decl_red_context.
Qed.

Lemma red1_it_mkLambda_or_LetIn_ctx {cf} {Σ} {wfΣ : wf Σ} Γ Δ Δ' u :
  OnOne2_local_env (on_one_decl (fun Δ : contextred1 Σ (Γ ,,, Δ))) Δ Δ'
  red1 Σ Γ (it_mkLambda_or_LetIn Δ u)
       (it_mkLambda_or_LetIn Δ' u).
Proof.
  induction 1 in u |- ×.
  - depelim p; subst; rewrite /it_mkLambda_or_LetIn /=. eapply red1_it_mkLambda_or_LetIn.
    simpl. now constructor.
  - depelim p; subst; rewrite /=; eapply red1_it_mkLambda_or_LetIn.
    destruct s as [[red ->]|[red ->]]; constructor; auto.
  - simpl. apply IHX.
Qed.


Lemma ctx_inst_merge {cf} {Σ} {wfΣ : wf Σ} Γ inst inst' Δ :
  wf_local Σ (Γ ,,, (List.rev Δ))
  PCUICTyping.ctx_inst
    (fun (Σ : global_env_ext) (Γ : context) (t T : term) ⇒
     u : term, closed_red1 Σ Γ t u Σ;;; Γ |- u : T) Σ Γ inst Δ
  ctx_inst Σ Γ inst Δ
  OnOne2 (closed_red1 Σ Γ) inst inst'
  ctx_inst Σ Γ inst' Δ.
Proof.
  intros wf c.
  induction c in inst', wf |- *; intros ctxi; depelim ctxi; intros o.
  - depelim o.
  - depelim o. constructor. apply t0. auto.
    rewrite -(List.rev_involutive Δ).
    rewrite subst_telescope_subst_context.
    simpl in wf. rewrite - !/(app_context _ _) app_context_assoc in wf.
    eapply ctx_inst_cumul.
    2:{ instantiate (1:=subst_context [i] 0 (List.rev Δ)).
        rewrite -subst_telescope_subst_context List.rev_involutive. exact ctxi. }
    eapply ws_cumul_ctx_pb_rel_app.
    eapply conv_cumul_context.
    eapply substitution_ws_cumul_ctx_pb_red_subst.
    now eapply wf_local_closed_context in wf.
    pose proof (wf_local_closed_context (typing_wf_local t2)).
    constructor; [|constructor].
    now eapply closed_red1_red.
    repeat constructor.
    specialize (t0 _ c0).
    eapply wf_local_app_inv, substitution_wf_local; tea.
    now eapply subslet_ass_tip.
    eapply wf_local_app_inv, substitution_wf_local; tea.
    now eapply subslet_ass_tip.
    constructor; auto. eapply IHc.
    rewrite -subst_context_subst_telescope.
    eapply substitution_wf_local; tea.
    repeat (constructor; tea). rewrite subst_empty; tea.
    simpl in wf. rewrite - !/(app_context _ _) app_context_assoc in wf.
    exact wf. tas. tas.
  - constructor. eapply IHc; eauto.
    simpl in wf. rewrite - !/(app_context _ _) app_context_assoc in wf.
    rewrite -subst_context_subst_telescope.
    eapply substitution_wf_local; tea.
    repeat (constructor; tea). eapply subslet_def. constructor.
    all:rewrite !subst_empty //.
    eapply wf_local_app_inv in wf as [wf _]. now depelim wf.
Qed.

Lemma ctx_inst_merge' {cf} {Σ} {wfΣ : wf Σ} Γ inst inst' Δ :
  wf_local Σ (Γ ,,, Δ)
  PCUICTyping.ctx_inst
    (fun (Σ : global_env_ext) (Γ : context) (t T : term) ⇒
     u : term, closed_red1 Σ Γ t u Σ;;; Γ |- u : T) Σ Γ inst (List.rev Δ)
  ctx_inst Σ Γ inst (List.rev Δ)
  OnOne2 (closed_red1 Σ Γ) inst inst'
  ctx_inst Σ Γ inst' (List.rev Δ).
Proof.
  intros. eapply ctx_inst_merge; try rewrite ?(List.rev_involutive Δ) //; tea.
Qed.

Lemma All2i_All2i_mix {A B} {P Q : nat A B Type}
      {n} {l : list A} {l' : list B} :
  All2i P n l l' All2i Q n l l' All2i (fun i x y ⇒ (P i x y × Q i x y)%type) n l l'.
Proof.
  induction 2; simpl; intros; constructor.
  inv X; intuition auto.
  apply IHX0. inv X; intuition auto.
Qed.

Definition conj_impl {A B} : A (A B) A × B := fun x f(x, f x).

Lemma is_open_term_snoc (Γ : context) M d : on_free_vars (shiftnP 1 (shiftnP #|Γ| xpred0)) M is_open_term (Γ ,, d) M.
Proof.
  rewrite /=.
  now rewrite [shiftnP (S #|Γ|) _]shiftnP_S.
Qed.

#[global] Hint Resolve is_open_term_snoc : fvs.

Ltac forward_keep H :=
  match type of H with
  ?X _
    let H' := fresh in
    assert (H' : X) ; [|specialize (H H')]
  end.
The subject reduction property of the system:

Definition SR_red1 {cf} Σ Γ t T :=
   u (Hu : closed_red1 Σ Γ t u), Σ ;;; Γ |- u : T.
  Ltac inv_on_free_vars :=
    match goal with
    | [ H : is_true (on_free_vars_decl _ _) |- _ ] ⇒ progress cbn in H
    | [ H : is_true (on_free_vars_decl _ (vdef _ _ _)) |- _ ] ⇒ unfold on_free_vars_decl, test_decl in H
    | [ H : is_true (_ && _) |- _ ] ⇒
      move/andP: H ⇒ []; intros
    | [ H : is_true (on_free_vars ?P ?t) |- _ ] ⇒
      progress (cbn in H || rewrite on_free_vars_mkApps in H);
      (move/and5P: H ⇒ [] || move/and4P: H ⇒ [] || move/and3P: H ⇒ [] || move/andP: H ⇒ [] ||
        eapply forallb_All in H); intros
    | [ H : is_true (test_def (on_free_vars ?P) ?Q ?x) |- _ ] ⇒
      move/andP: H ⇒ []; rewrite ?shiftnP_xpredT; intros
    | [ H : is_true (test_context_k _ _ _ ) |- _ ] ⇒
      rewritetest_context_k_closed_on_free_vars_ctx in H
    end.

Lemma closed_red1_ind (Σ : global_env_ext) (P0 : context term term Type)
  (P := fun Γ t uis_closed_context Γ is_open_term Γ t P0 Γ t u) :
  ( (Γ : context) (na : aname) (t b a : term),
    P Γ (tApp (tLambda na t b) a) (b {0 := a}))

  ( (Γ : context) (na : aname) (b t b' : term), P Γ (tLetIn na b t b') (b' {0 := b}))

  ( (Γ : context) (i : nat) (body : term),
  option_map decl_body (nth_error Γ i) = Some (Some body) P Γ (tRel i) ((lift0 (S i)) body))

  ( (Γ : context) (ci : case_info) (c : nat) (u : Instance.t) (args : list term)
    (p : predicate term) (brs : list (branch term)) br,
    nth_error brs c = Some br
    #|args| = (ci.(ci_npar) + context_assumptions br.(bcontext))%nat
    P Γ (tCase ci p (mkApps (tConstruct ci.(ci_ind) c u) args) brs)
        (iota_red ci.(ci_npar) p args br))

  ( (Γ : context) (mfix : mfixpoint term) (idx : nat) (args : list term) (narg : nat) (fn : term),
  unfold_fix mfix idx = Some (narg, fn)
  is_constructor narg args = true P Γ (mkApps (tFix mfix idx) args) (mkApps fn args))

  ( (Γ : context) ci (p : predicate term) (mfix : mfixpoint term) (idx : nat)
    (args : list term) (narg : nat) (fn : term) (brs : list (branch term)),
  unfold_cofix mfix idx = Some (narg, fn)
  P Γ (tCase ci p (mkApps (tCoFix mfix idx) args) brs) (tCase ci p (mkApps fn args) brs))

  ( (Γ : context) (p : projection) (mfix : mfixpoint term) (idx : nat) (args : list term)
    (narg : nat) (fn : term),
  unfold_cofix mfix idx = Some (narg, fn) P Γ (tProj p (mkApps (tCoFix mfix idx) args)) (tProj p (mkApps fn args)))

  ( (Γ : context) c (decl : constant_body) (body : term),
  declared_constant Σ c decl
   u : Instance.t, cst_body decl = Some body P Γ (tConst c u) (subst_instance u body))

  ( (Γ : context) p (args : list term) (u : Instance.t)
    (arg : term),
      nth_error args (p.(proj_npars) + p.(proj_arg)) = Some arg
      P Γ (tProj p (mkApps (tConstruct p.(proj_ind) 0 u) args)) arg)

  ( (Γ : context) (na : aname) (M M' N : term),
  closed_red1 Σ Γ M M' P0 Γ M M' P Γ (tLambda na M N) (tLambda na M' N))

  ( (Γ : context) (na : aname) (M M' N : term),
  closed_red1 Σ (Γ,, vass na N) M M' P0 (Γ,, vass na N) M M'
  P Γ (tLambda na N M) (tLambda na N M'))

  ( (Γ : context) (na : aname) (b t b' r : term),
  closed_red1 Σ Γ b r P0 Γ b r P Γ (tLetIn na b t b') (tLetIn na r t b'))

  ( (Γ : context) (na : aname) (b t b' r : term),
  closed_red1 Σ Γ t r P0 Γ t r P Γ (tLetIn na b t b') (tLetIn na b r b'))

  ( (Γ : context) (na : aname) (b t b' r : term),
  closed_red1 Σ (Γ,, vdef na b t) b' r P0 (Γ,, vdef na b t) b' r P Γ (tLetIn na b t b') (tLetIn na b t r))

  ( (Γ : context) (ci : case_info) p params' c brs,
    OnOne2 (Trel_conj (closed_red1 Σ Γ) (P0 Γ)) p.(pparams) params'
      P Γ (tCase ci p c brs)
          (tCase ci (set_pparams p params') c brs))

  
  ( (Γ : context) (ci : case_info) p preturn' c brs,
    closed_red1 Σ (Γ ,,, inst_case_predicate_context p) p.(preturn) preturn'
    P0 (Γ ,,, inst_case_predicate_context p) p.(preturn) preturn'
    P Γ (tCase ci p c brs)
        (tCase ci (set_preturn p preturn') c brs))
  
  ( (Γ : context) (ind : case_info) (p : predicate term) (c c' : term) (brs : list (branch term)),
  closed_red1 Σ Γ c c' P0 Γ c c' P Γ (tCase ind p c brs) (tCase ind p c' brs))

  ( (Γ : context) ci p c brs brs',
    OnOne2 (fun br br'
    (on_Trel_eq (Trel_conj (closed_red1 Σ (Γ ,,, inst_case_branch_context p br))
      (P0 (Γ ,,, inst_case_branch_context p br)))
      bbody bcontext br br')) brs brs'
    P Γ (tCase ci p c brs) (tCase ci p c brs'))

  ( (Γ : context) (p : projection) (c c' : term),
    closed_red1 Σ Γ c c' P0 Γ c c'
    P Γ (tProj p c) (tProj p c'))

  ( (Γ : context) (M1 N1 : term) (M2 : term),
  closed_red1 Σ Γ M1 N1 P0 Γ M1 N1
  P Γ (tApp M1 M2) (tApp N1 M2))

  ( (Γ : context) (M2 N2 : term) (M1 : term),
  closed_red1 Σ Γ M2 N2 P0 Γ M2 N2
  P Γ (tApp M1 M2) (tApp M1 N2))

  ( (Γ : context) (na : aname) (M1 M2 N1 : term),
  closed_red1 Σ Γ M1 N1 P0 Γ M1 N1
  P Γ (tProd na M1 M2) (tProd na N1 M2))

  ( (Γ : context) (na : aname) (M2 N2 M1 : term),
  closed_red1 Σ (Γ,, vass na M1) M2 N2
  P0 (Γ,, vass na M1) M2 N2
  P Γ (tProd na M1 M2) (tProd na M1 N2))

  ( (Γ : context) (ev : nat) (l l' : list term),
      OnOne2 (Trel_conj (closed_red1 Σ Γ) (P0 Γ)) l l'
      P Γ (tEvar ev l) (tEvar ev l'))

  ( (Γ : context) (mfix0 mfix1 : list (def term)) (idx : nat),
  OnOne2 (on_Trel_eq (Trel_conj (closed_red1 Σ Γ) (P0 Γ)) dtype (fun x(dname x, dbody x, rarg x))) mfix0 mfix1
  P Γ (tFix mfix0 idx) (tFix mfix1 idx))

  ( (Γ : context) (mfix0 mfix1 : list (def term)) (idx : nat),
  OnOne2 (on_Trel_eq (Trel_conj (closed_red1 Σ (Γ ,,, fix_context mfix0))
                                (P0 (Γ ,,, fix_context mfix0))) dbody
                      (fun x(dname x, dtype x, rarg x))) mfix0 mfix1
  P Γ (tFix mfix0 idx) (tFix mfix1 idx))

  ( (Γ : context) (mfix0 mfix1 : list (def term)) (idx : nat),
  OnOne2 (on_Trel_eq (Trel_conj (closed_red1 Σ Γ) (P0 Γ)) dtype (fun x(dname x, dbody x, rarg x))) mfix0 mfix1
  P Γ (tCoFix mfix0 idx) (tCoFix mfix1 idx))

  ( (Γ : context) (mfix0 mfix1 : list (def term)) (idx : nat),
  OnOne2 (on_Trel_eq (Trel_conj (closed_red1 Σ (Γ ,,, fix_context mfix0))
                                (P0 (Γ ,,, fix_context mfix0))) dbody
                      (fun x(dname x, dtype x, rarg x))) mfix0 mfix1
  P Γ (tCoFix mfix0 idx) (tCoFix mfix1 idx))
  
   (Γ : context) (t t0 : term), closed_red1 Σ Γ t t0 P0 Γ t t0.
Proof.
  intros.
  destruct X27 as [clΓ clt r].
  move: clΓ clt.
  Ltac t :=
    eauto; try split; eauto;
    try apply on_free_vars_ctx_snoc_ass ⇒ //;
    try apply on_free_vars_ctx_snoc_def ⇒ //;
    try apply is_open_term_snoc ⇒ //;
    repeat (try inv_on_free_vars; eauto with fvs; cbn).
  induction r using red1_ind_all; intros;
    try solve [multimatch goal with
    | H : _ |- _eapply H
    end; t].
  - eapply X13. 2-3:t.
    inv_on_free_vars.
    eapply forallb_All in p0.
    eapply OnOne2_All_mix_left in X27; tea.
    eapply OnOne2_impl; tea; repeat (intuition auto; t).
  - forward_keep IHr.
    { rewrite on_free_vars_ctx_app clΓ.
      eapply on_free_vars_ctx_inst_case_context; trea; t. }
    forward_keep IHr.
    { repeat inv_on_free_vars.
      rewrite app_length inst_case_predicate_context_length -shiftnP_add //. }
    apply X14 ⇒ //.
  - eapply X16 ⇒ //.
    inv_on_free_vars.
    eapply forallb_All in p4.
    eapply OnOne2_All_mix_left in X27; tea. cbn in X27.
    eapply OnOne2_impl; tea; cbn; intros ?? [[[]] ?].
    forward_keep p5.
    { rewrite on_free_vars_ctx_app clΓ /=.
      eapply on_free_vars_ctx_inst_case_context; trea; t. }
    forward_keep p5.
    { repeat inv_on_free_vars.
      rewrite app_length inst_case_branch_context_length -shiftnP_add //. }
    intuition auto. split; auto.
  - eapply X22 ⇒ //.
    cbn in clt. eapply forallb_All in clt.
    eapply OnOne2_All_mix_left in X27; tea.
    eapply OnOne2_impl; tea; cbn; intuition auto; t.
  - eapply X23 ⇒ //.
    cbn in clt. eapply forallb_All in clt.
    eapply OnOne2_All_mix_left in X27; tea.
    eapply OnOne2_impl; tea; cbn; intuition auto; t.
  - eapply X24 ⇒ //.
    cbn in clt. eapply forallb_All in clt.
    eapply OnOne2_All_mix_left in X27; tea.
    eapply OnOne2_impl; tea; cbn; intros ?? [[[]] ?].
    forward_keep p.
    { rewrite on_free_vars_ctx_app clΓ /=.
      eapply on_free_vars_fix_context; trea; t. }
    forward_keep p. {
      rewrite app_length fix_context_length -shiftnP_add //.
      now inv_on_free_vars. }
    intuition auto. split; auto.
  - eapply X25 ⇒ //.
    cbn in clt. eapply forallb_All in clt.
    eapply OnOne2_All_mix_left in X27; tea.
    eapply OnOne2_impl; tea; cbn; intuition auto; t.
  - eapply X26 ⇒ //.
    cbn in clt. eapply forallb_All in clt.
    eapply OnOne2_All_mix_left in X27; tea.
    eapply OnOne2_impl; tea; cbn; intros ?? [[[]] ?].
    forward_keep p.
    { rewrite on_free_vars_ctx_app clΓ /=.
      eapply on_free_vars_fix_context; trea; t. }
    forward_keep p. {
      rewrite app_length fix_context_length -shiftnP_add //.
      now inv_on_free_vars. }
    intuition auto. split; auto.
Qed.

Definition closed_red1_ind' :=
    ltac:(let T := type of closed_red1_ind in
    let T' := eval cbn in T in
      exact (closed_red1_ind : T')).

Ltac invert_closed_red H :=
  generalize_eqs H; destruct H using closed_red1_ind'; simplify_dep_elim.

Ltac invert_mkApps_fix_eq :=
  match goal with
  | [ H : mkApps (tFix _ _) _ = _ |- _ ] ⇒
    apply mkApps_Fix_spec in H; noconf H
  end.

Coercion closed_red1_red : closed_red1 >-> closed_red.

Lemma wt_cumul_pb_refl {cf} {Σ} {wfΣ : wf Σ} {Γ t T} : Σ ;;; Γ |- t : T Σ ;;; Γ t = t.
Proof.
  intros. apply ws_cumul_pb_refl.
  apply wf_local_closed_context; pcuic.
  now apply subject_closed in X; apply closedn_on_free_vars.
Qed.

Lemma ws_cumul_pb_meta_refl {cf} {Σ} {wfΣ : wf Σ} {Γ T U} :
  is_closed_context Γ closedn #|Γ| T T = U Σ ;;; Γ T = U.
Proof.
  intros clΓ cl →. apply ws_cumul_pb_refl ⇒ //. now apply closedn_on_free_vars.
Qed.

Lemma ws_cumul_pb_eq_trans {cf} {Σ} {wfΣ : wf Σ} {Γ T U V} :
  Σ ;;; Γ T = U U = V Σ ;;; Γ T = V.
Proof.
  now intros tr →.
Qed.

Lemma eq_ws_cumul_pb_trans {cf} {Σ} {wfΣ : wf Σ} {Γ T U V} :
  T = U Σ ;;; Γ U = V Σ ;;; Γ T = V.
Proof.
  now introstr.
Qed.

Lemma ws_cumul_pb_terms_eq_trans {cf} {Σ} {wfΣ : wf Σ} {Γ T U V} :
  ws_cumul_pb_terms Σ Γ T U U = V ws_cumul_pb_terms Σ Γ T V.
Proof.
  now intros tr →.
Qed.

Lemma eq_ws_cumul_pb_terms_trans {cf} {Σ} {wfΣ : wf Σ} {Γ T U V} :
  T = U ws_cumul_pb_terms Σ Γ U V ws_cumul_pb_terms Σ Γ T V.
Proof.
  now introstr.
Qed.

Lemma red_terms_refl {Σ Γ ts} :
  is_closed_context Γ
  forallb (is_open_term Γ) ts red_terms Σ Γ ts ts.
Proof.
  solve_all.
  eapply All_All2; tea. cbn.
  firstorder auto.
Qed.

Local Notation welltyped Σ Γ t := ( T, Σ ;;; Γ |- t : T).
Local Notation welltyped_terms Σ Γ := (All (fun twelltyped Σ Γ t)).

Lemma spine_subst_wt_terms {cf} {Σ Γ inst s Δ} : spine_subst Σ Γ inst s Δ
  welltyped_terms Σ Γ inst.
Proof.
  move/spine_subst_ctx_inst.
  induction 1; try constructor; auto.
  now t.
Qed.

Lemma wt_terms_ws_cumul_pb {cf} {Σ} {wfΣ : wf Σ} {Γ ts} : welltyped_terms Σ Γ ts ws_cumul_pb_terms Σ Γ ts ts.
Proof.
  intros; eapply All_All2; tea. cbn; intros x [T HT].
  now eapply wt_cumul_pb_refl.
Qed.

Lemma weakening_ws_cumul_ctx_pb {cf} {Σ} {wfΣ : wf Σ} {Γ Δ Δ0 Δ1} :
  Σ Γ ,,, Δ0 = Γ ,,, Δ1
  Σ Γ ,,, Δ = Γ ,,, Δ
  Σ Γ ,,, Δ ,,, lift_context #|Δ| 0 Δ0 = Γ ,,, Δ ,,, lift_context #|Δ| 0 Δ1.
Proof.
  intros h h'.
  eapply ws_cumul_ctx_pb_rel_app.
  eapply ws_cumul_ctx_pb_rel_app in h.
  induction h.
  induction b; cbn. constructor. fvs.
  constructor.
  depelim p; cbn; rewrite !lift_context_snoc; constructor; auto; fvs;
  rewrite /lift_decl /map_decl /=; constructor; auto with fvs. apply IHb.
  constructor; auto. rewrite !Nat.add_0_r. rewrite -(All2_fold_length b).
  eapply weakening_ws_cumul_pb ⇒ //. fvs. apply IHb.
  constructor; auto; rewrite !Nat.add_0_r -(All2_fold_length b);
  apply weakening_ws_cumul_pb ⇒ //; fvs.
Qed.

Lemma on_constructor_closed_indices {cf} {Σ} {wfΣ : wf Σ} :
   {i mdecl idecl cdecl},
  declared_constructor Σ.1 i mdecl idecl cdecl
  All (is_open_term (arities_context (ind_bodies mdecl) ,,, ind_params mdecl ,,, cstr_args cdecl)) (cstr_indices cdecl).
Proof.
  intros.
  pose proof (on_declared_constructor H) as [[onmind oib] [cs [hnth onc]]].
  pose proof (onc.(on_cindices)).
  now eapply ctx_inst_open_terms in X.
Qed.

Lemma on_constructor_wf_arities_pars_args {cf} {Σ} {wfΣ : wf Σ} {i mdecl idecl cdecl} :
  declared_constructor Σ.1 i mdecl idecl cdecl
  wf_local (Σ.1, ind_universes mdecl) (arities_context (ind_bodies mdecl) ,,, ind_params mdecl ,,, cstr_args cdecl).
Proof.
  moveH.
  pose proof (on_declared_constructor H) as [[onmind oib] [cs [hnth onc]]].
  move/on_cargs/sorts_local_ctx_wf_local: oncH'.
  apply H'.
  apply weaken_wf_local; tea.
  eapply (wf_arities_context H).
  now apply onParams in onmind.
Qed.

Lemma closedP_shiftnP_eq k : closedP k xpredT =1 shiftnP k xpred0.
Proof.
  rewrite /closedP /shiftnP. intros i; nat_compare_specs ⇒ //.
Qed.

Lemma on_free_vars_closedn k t : closedn k t = on_free_vars (shiftnP k xpred0) t.
Proof.
  rewrite closedP_on_free_vars.
  eapply on_free_vars_ext, closedP_shiftnP_eq.
Qed.

Lemma on_constructor_closed_indices_inst {cf} {Σ} {wfΣ : wf Σ} {i mdecl idecl cdecl u} :
  declared_constructor Σ.1 i mdecl idecl cdecl
  consistent_instance_ext Σ (ind_universes mdecl) u
  All (is_open_term (ind_params mdecl ,,, cstr_args cdecl)@[u])
    (map (subst (inds (inductive_mind (fst i)) u (ind_bodies mdecl))
           (#|cstr_args cdecl| + #|ind_params mdecl|)) (cstr_indices cdecl)@[u]).
Proof.
  intros H cu.
  pose proof (on_declared_constructor H) as [[onmind oib] [cs [hnth onc]]].
  pose proof (onc.(on_cindices)).
  eapply ctx_inst_inst in X; tea.
  eapply ctx_inst_open_terms in X.
  eapply All_map, All_impl; tea.
  cbn; intros x clx.
  rewrite -[_ ,,, _]app_context_nil_l -[_ ,,, cstr_args cdecl]app_context_assoc app_context_assoc in clx.
  rewrite !subst_instance_app_ctx in clx.
  eapply (is_open_term_subst (Γ := []) (s:=inds (inductive_mind i.1) u (ind_bodies mdecl))) in clx.
  3:eapply inds_is_open_terms. 3:len.
  rewrite app_context_nil_l subst_context_app in clx.
  rewrite closed_ctx_subst in clx.
  now eapply declared_inductive_closed_params_inst.
  len in clx. len.
  rewrite app_context_nil_l app_context_assoc.
  epose proof (on_constructor_wf_arities_pars_args H).
  eapply (wf_local_instantiate (decl:=InductiveDecl mdecl)) in X0; tea.
  rewrite !subst_instance_app_ctx in X0.
  now eapply wf_local_closed_context in X0. apply H.
  now eapply declared_inductive_wf_global_ext.
Qed.

Arguments pair {A B}%type_scope &.

Lemma ws_cumul_pb_terms_refl {cf} {Σ} {wfΣ : wf Σ} {Γ u} :
  is_closed_context Γ
  forallb (is_open_term Γ) u
  ws_cumul_pb_terms Σ Γ u u.
Proof.
  intros. eapply into_ws_cumul_pb_terms ⇒ //.
  eapply All2_refl; reflexivity.
Qed.

Lemma All2_tip {A} {P} (t u : A) : P t u All2 P [t] [u].
Proof. now repeat constructor. Qed.
#[global] Hint Resolve All2_tip : core.

Lemma map2_set_binder_name_expand_lets nas Γ Δ :
  #|nas| = #|Δ|
  map2 set_binder_name nas (expand_lets_ctx Γ Δ) =
  expand_lets_ctx Γ (map2 set_binder_name nas Δ).
Proof.
  movehlen.
  rewrite /expand_lets_ctx /expand_lets_k_ctx.
  rewrite PCUICRenameConv.map2_set_binder_name_fold ?lengths //.
  rewrite PCUICRenameConv.map2_set_binder_name_fold ?lengths //.
Qed.

Lemma closed_red1_eq_context_upto_names {Σ Γ Γ'} {t u} :
  eq_context_upto_names Γ Γ' closed_red1 Σ Γ t u closed_red1 Σ Γ' t u.
Proof.
  intros eqctx []; split; auto.
  - eapply eq_context_upto_names_on_free_vars; tea.
  - now rewrite -(All2_length eqctx).
  - eapply red1_eq_context_upto_names; tea.
Qed.

Lemma closed_red1_ws_cumul_pb {cf} {Σ} {wfΣ : wf Σ} {Γ} {t u} :
  closed_red1 Σ Γ t u ws_cumul_pb Conv Σ Γ t u.
Proof.
  intros cl. now eapply red_conv, closed_red1_red.
Qed.

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

Lemma on_free_vars_ctx_tip P d : on_free_vars_ctx P [d] = on_free_vars_decl P d.
Proof. cbn; rewrite andb_true_r // shiftnP0 //. Qed.

Lemma on_free_vars_it_mkLambda_or_LetIn {P Δ t} :
  on_free_vars P (it_mkLambda_or_LetIn Δ t) =
    on_free_vars_ctx P Δ && on_free_vars (shiftnP #|Δ| P) t.
Proof.
  move: P. induction Δ using rev_indP.
  - cbn. now rewrite shiftnP0.
  - destruct x as [na [b|] ty]; rewrite it_mkLambda_or_LetIn_app /= /mkLambda_or_LetIn /=.
    rewrite on_free_vars_ctx_app /= IHΔ !lengths /= shiftnP_add on_free_vars_ctx_tip /=
      /on_free_vars_decl /test_decl /=. ring.
    rewrite on_free_vars_ctx_app /= IHΔ !lengths /= shiftnP_add on_free_vars_ctx_tip /=
     /on_free_vars_decl /test_decl /=. ring.
Qed.

Lemma closed_red1_it_mkLambda_or_LetIn {cf} {Σ} {wfΣ : wf Σ} {Γ} {Δ t u} :
  Σ ;;; Γ ,,, Δ t ⇝1 u Σ ;;; Γ it_mkLambda_or_LetIn Δ t ⇝1 it_mkLambda_or_LetIn Δ u.
Proof.
  intros [clΓΔ opt r].
  split; eauto with fvs.
  - rewrite on_free_vars_ctx_app in clΓΔ. now move/andP: clΓΔ.
  - rewrite on_free_vars_it_mkLambda_or_LetIn.
    rewrite on_free_vars_ctx_app in clΓΔ. move/andP: clΓΔ ⇒ [].
    rewrite shiftnP_add -app_length opt andb_true_r //.
  - now eapply red1_it_mkLambda_or_LetIn.
Qed.

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

Lemma weakening_closed_red1 {cf} {Σ} {wfΣ : wf Σ} {Γ Γ' Γ'' : context} {M N} :
  closed_red1 Σ (Γ,,, Γ') M N
  is_closed_context (Γ ,,, Γ'')
  closed_red1 Σ (Γ,,, Γ'',,, lift_context #|Γ''| 0 Γ') (lift #|Γ''| #|Γ'| M) (lift #|Γ''| #|Γ'| N).
Proof.
  intros r cl. split ⇒ //.
  apply is_closed_context_lift ⇒ //. apply r.
  apply is_open_term_lift, r.
  apply weakening_red1 ⇒ //. eapply on_free_vars_impl, r ⇒ //.
  apply r.
Qed.

Lemma closed_red1_case_branch_type {cf} {Σ} {wfΣ : wf Σ} {Γ} {ret ret'} {ind mdecl idecl k cdecl br p} :
  let cb := case_branch_type ind mdecl idecl p br ret k cdecl in
  let cb' := case_branch_type ind mdecl idecl p br ret' k cdecl in
  wf_branch cdecl br
  is_open_term (Γ ,,, cb.1) cb.2
  is_closed_context (Γ ,,, cb.1)
  Σ ;;; Γ ret ⇝1 ret'
  Σ ;;; Γ ,,, cb.1 cb.2 ⇝1 cb'.2.
Proof.
  intros cb cb' wfbr op r.
  split ⇒ //.
  eapply closed_red1_mkApps_left ⇒ //.
  - relativize #|cstr_args cdecl|; [eapply (weakening_closed_red1 (Γ':=[]))|] ⇒ //.
    apply (case_branch_context_length_args wfbr).
  - move: op; rewrite on_free_vars_mkApps ⇒ /andP[] //.
Qed.

Lemma inst_case_branch_context_eq {cf} {Σ} {wfΣ : wf Σ} {p br} {ind mdecl cdecl} :
  declared_minductive Σ (inductive_mind ind) mdecl
  consistent_instance_ext Σ (ind_universes mdecl) p.(puinst)
  eq_context_upto_names br.(bcontext) (cstr_branch_context ind mdecl cdecl)
  eq_context_upto_names (inst_case_branch_context p br) (pre_case_branch_context ind mdecl p.(pparams) p.(puinst) cdecl).
Proof.
  intros declm cu eqbr.
  rewrite /inst_case_branch_context /pre_case_branch_context.
  rewrite /inst_case_context.
  eapply alpha_eq_subst_context.
  etransitivity; tea.
  - eapply alpha_eq_subst_instance; tea.
  - rewrite /cstr_branch_context subst_instance_expand_lets_ctx subst_instance_subst_context //.
    rewrite instantiate_inds //.
    reflexivity.
Qed.

Lemma skipn_nil_length {A} (l : list A) n : skipn n l = [] #|l| n.
Proof.
  induction n in l |- *; destruct l; simpl; rewrite ?skipn_0 ?skipn_S; auto; try congruence; try lia.
  intros hs. specialize (IHn _ hs). lia.
Qed.

Lemma context_assumptions_bound Γ : context_assumptions Γ #|Γ|.
Proof.
  induction Γ as [|[? [] ?] ?]; intros; cbn; lia.
Qed.

Lemma declared_projection_indices {cf} {Σ} {wfΣ : wf Σ} {p mdecl idecl cdecl pdecl} :
  declared_projection Σ p mdecl idecl cdecl pdecl
  #|ind_indices idecl| = 0.
Proof.
  moveisdecl.
  case: (on_declared_projection isdecl) ⇒ onind. cbn.
  destruct ind_cunivs as [] ⇒ /= // ⇒ [] [] [] [] //.
  destruct l as [] ⇒ //. intros sorts onprojs hp.
  now destruct onprojs.
Qed.

Lemma map_subst_lift0_subst s k l : map (subst s k lift0 k) l = map (lift0 k subst0 s) l.
Proof.
  eapply map_extx. now rewrite subst_lift_subst.
Qed.

Lemma substitution_ws_cumul_pb_subst_conv {cf} {Σ} {wfΣ : wf Σ} {le Γ Γ0 Γ1 Δ s s' T U} :
  subslet Σ Γ s Γ0
  wf_subslet Σ Γ s' Γ1
  ws_cumul_pb_terms Σ Γ s s'
  Σ;;; Γ ,,, Γ0 ,,, Δ T ≤[le] U
  Σ;;; Γ ,,, subst_context s 0 Δ subst s #|Δ| T ≤[le] subst s' #|Δ| U.
Proof.
  intros subs subs' eq.
  eapply substitution_ws_cumul_pb_subst_conv; tea.
  × now eapply subslet_untyped_subslet.
  × eapply subslet_untyped_subslet, subs'.
  × eapply wf_local_closed_context, subs'.
Qed.

Lemma wf_subslet_skipn {cf Σ Γ s Δ n} :
  wf_subslet Σ Γ s Δ wf_subslet Σ Γ (skipn n s) (skipn n Δ).
Proof.
  intros []; split; auto using subslet_skipn.
  now eapply wf_local_app_skipn.
Qed.

Lemma isType_subst_arities {cf} {Σ} {wfΣ : wf Σ} {ind mdecl idecl u} {Γ T} :
  declared_inductive Σ ind mdecl idecl
  consistent_instance_ext Σ (ind_universes mdecl) u
  isType Σ ((arities_context (ind_bodies mdecl))@[u] ,,, Γ) T
  isType Σ (subst_context (ind_subst mdecl ind u) 0 Γ) (subst (ind_subst mdecl ind u) #|Γ| T).
Proof.
  intros isdecl cu.
  rewrite -[_ ,,, _]app_context_nil_l app_context_assoc.
  move/(isType_substitution (subslet_inds isdecl cu)).
  rewrite app_context_nil_l //.
Qed.

Lemma wt_closed_red1 {cf} {Σ} {wfΣ : wf Σ} {Γ T U} :
  welltyped Σ Γ T
  red1 Σ Γ T U
  Σ ;;; Γ T ⇝1 U.
Proof.
  intros [ty HT] r.
  split ⇒ //.
  eapply wf_local_closed_context; pcuic.
  now eapply subject_is_open_term in HT.
Qed.

Lemma isType_expand_lets {cf} {Σ} {wfΣ : wf Σ} {Γ Δ T} :
  isType Σ (Γ ,,, Δ) T
  isType Σ (smash_context [] Γ ,,, expand_lets_ctx Γ Δ) (expand_lets_k Γ #|Δ| T).
Proof.
  move⇒ [] s.
  rewrite -[_ ,,, _]app_context_nil_l app_context_assoc.
  move/typing_expand_lets_gen; rewrite app_context_nil_lhs.
  now s.
Qed.

Lemma isType_subst_extended_subst {cf} {Σ} {wfΣ : wf Σ} {Γ Δ T} :
  isType Σ (Γ ,,, Δ) T
  isType Σ (smash_context [] Γ ,,, subst_context (extended_subst Γ 0) 0 Δ)
    (subst (extended_subst Γ 0) #|Δ| T).
Proof.
  move⇒ [] s.
  intros Hs.
  have wfctx := typing_wf_local Hs.
  generalize Hs.
  rewrite -[_ ,,, _]app_context_nil_l app_context_assoc.
  move/typing_expand_lets_gen; rewrite app_context_nil_lhs.
   s.
  rewrite /expand_lets_ctx /expand_lets_k_ctx in hs.
  rewrite closed_ctx_lift /= in hs.
  move/closed_wf_local: wfctx. rewrite closedn_ctx_app ⇒ /andP[] //.
  rewrite /expand_lets_k /= in hs.
  rewrite lift_closed in hs. eapply subject_closed in Hs.
  now len in Hs.
  apply hs.
Qed.

Lemma isType_mkApps_Ind_proj_inv {cf:checker_flags} {Σ Γ p u pars} (wfΣ : wf Σ.1)
  {mdecl idecl cdecl pdecl} (declm : declared_projection Σ.1 p mdecl idecl cdecl pdecl) :
  isType Σ Γ (mkApps (tInd p.(proj_ind) u) pars)
    let parctx := (subst_instance u (ind_params mdecl)) in
     spine_subst Σ Γ pars (List.rev pars) (smash_context [] parctx),
       #|pars| = ind_npars mdecl,
       idecl.(ind_indices) = [] &
       consistent_instance_ext Σ (ind_universes mdecl) u].
Proof.
  moveisTy. generalize isTy. apply isType_wf_local in isTy.
  move/(isType_mkApps_Ind_inv _ declm isTy) ⇒ [parsubst [argsubst [sp sargs hp hargs cu]]].
  generalize (declared_projection_indices declm).
  move/length_nilhindices.
  move: hargs; rewrite hindices /=.
  move/length_nil/skipn_nil_length.
  move/firstn_length_le_inv: hphle hge.
  have heq: #|pars| = ind_npars mdecl by lia.
  split ⇒ //.
  rewrite -heq in sp.
  rewrite firstn_all in sp.
  now apply: spine_subst_smash.
Qed.

Lemma type_Cumul_alt {cf} {Σ} {wfΣ : wf Σ} (Γ : context) (t T T' : term) :
  Σ;;; Γ |- t : T isType Σ Γ T'
  Σ;;; Γ |- T T' Σ;;; Γ |- t : T'.
Proof.
  intros Ht isty cum.
  eapply (type_ws_cumul_pb (pb:=Cumul)); tea.
  eapply into_ws_cumul_pb; fvs.
Qed.

Lemma sr_red1 {cf:checker_flags} :
  env_prop SR_red1
      (fun Σ Γwf_local Σ Γ ×
        ( Γ' Δ' Δ,
          Γ = Γ' ,,, Δ'
          OnOne2_local_env (on_one_decl (fun Δ : contextclosed_red1 Σ (Γ',,, Δ))) Δ' Δ
          wf_local_rel Σ Γ' Δ)).
Proof.
  apply typing_ind_env; intros Σ wfΣ Γ wfΓ; unfold SR_red1; intros **; rename_all_hyps; auto.
  2-15:match goal with
    | [H : (_ ;;; _ |- _ s _) |- _ ] ⇒ idtac
    | _
      invert_closed_red Hu;
      try solve [invert_mkApps_fix_eq];
      try solve [econstructor; eauto];
      try solve [
        match goal with
        | h : _ = mkApps _ ?args |- _
          let e := fresh "e" in
          apply (f_equal nApp) in h as e ; simpl in e ;
          rewrite nApp_mkApps in e ; simpl in e ;
          destruct args ; discriminate
        end
      ]
    end.

  -
    split; auto. intros Γ' Δ' Δ →.
    induction 1.
    × depelim p. subst. depelim X. constructor.
      now eapply wf_local_app_inv.
      apply infer_typing_sort_impl with id tu; intros _.
      now eapply Hs.
    × depelim X.
      constructor. now eapply wf_local_app_inv.
      depelim p. destruct s as [[red <-]|[red <-]]; subst.
      apply infer_typing_sort_impl with id tu; intros _.
      now eapply Hs.
      exact tu.
      red. depelim p. destruct s as [[red <-]|[red <-]]; subst.
      specialize (Hs _ red). eapply type_ws_cumul_pb; tea.
      apply infer_typing_sort_impl with id tu; intros _.
      apply Hs. eapply (red_ws_cumul_pb (pb:=Cumul)).
      now eapply closed_red1_red.
      now eapply Hc.

    × depelim X; specialize (IHX0 _ X); pose proof (wf_local_closed_context all).
      + constructor; auto. clear X.
        pose proof (wf_local_closed_context all).
        eapply wf_local_app_inv in all as [].
        eapply wf_local_app in IHX0; tea.
        apply infer_typing_sort_impl with id tu; intros Hty.
        eapply closed_context_conversion; tea.
        eapply red_one_decl_ws_cumul_ctx_pb ⇒ //.
        eapply OnOne2_local_env_impl; tea.
        intros ???. eapply on_one_decl_impl ⇒ ???; firstorder.
      + constructor; auto. clear X.
        { eapply wf_local_app_inv in all as [].
          eapply wf_local_app in IHX0; tea.
          apply infer_typing_sort_impl with id tu; intros Hty.
          eapply closed_context_conversion; tea.
          eapply red_one_decl_ws_cumul_ctx_pb ⇒ //.
          eapply OnOne2_local_env_impl; tea.
          intros ???. eapply on_one_decl_impl ⇒ ???; firstorder. }
        { red.
          clear X; eapply wf_local_app_inv in all as [].
          eapply wf_local_app in IHX0; tea.
          eapply closed_context_conversion; tea.
          eapply red_one_decl_ws_cumul_ctx_pb ⇒ //.
          eapply OnOne2_local_env_impl; tea.
          intros ???. eapply on_one_decl_impl ⇒ ???; firstorder. }

  -
    rewrite heq_nth_error in H. destruct decl as [na b ty]; noconf H.
    simpl.
    pose proof (PCUICValidity.nth_error_All_local_env heq_nth_error wfΓ); eauto.
    cbn in ×.
    rewrite <- (firstn_skipn (S n) Γ).
    eapply weakening_length; auto.
    { rewrite firstn_length_le; auto. apply nth_error_Some_length in heq_nth_error. auto with arith. }
    now unfold app_context; rewrite firstn_skipn.

  -
    constructor; eauto. intuition auto.
    unshelve eapply (closed_context_conversion _ typeb); pcuics.
    constructor. now eapply ws_cumul_ctx_pb_refl, wf_local_closed_context.
    constructor; auto. eapply red_conv.
    now eapply closed_red1_red.

  -
    eapply type_Cumul_alt. eapply type_Lambda; eauto.
    intuition auto.
    unshelve eapply (closed_context_conversion _ typeb); pcuics.
    constructor. now eapply ws_cumul_ctx_pb_refl, wf_local_closed_context.
    constructor; auto. eapply red_conv. now eapply closed_red1_red.
    assert (Σ ;;; Γ |- tLambda n t b : tProd n t bty). econstructor; pcuics.
    now eapply validity in X0.
    econstructor 3. eapply cumul_refl'.
    constructor. apply Hu.

  -
    eapply type_Cumul_alt.
    apply (@substitution_let _ _ _ Γ n b b_ty b' b'_ty typeb').
    specialize (typing_wf_local typeb') as wfd.
    assert (Σ ;;; Γ |- tLetIn n b b_ty b' : tLetIn n b b_ty b'_ty).
    econstructor; eauto.
    eapply (validity X0).
    eapply cumul_red_r.
    apply cumul_refl'. constructor.

  -
    eapply type_Cumul_alt.
    econstructor; eauto.
    unshelve eapply (closed_context_conversion _ typeb'); pcuics.
    constructor. eapply ws_cumul_ctx_pb_refl; eauto. constructor; auto.
    now eapply red_conv, closed_red1_red. apply ws_cumul_pb_refl; eauto. now repeat inv_on_free_vars.
    assert (Σ ;;; Γ |- tLetIn n b b_ty b' : tLetIn n b b_ty b'_ty). econstructor; eauto.
    eapply (validity X0).
    eapply cumul_red_r.
    apply cumul_refl'. constructor. apply Hu.

  -
    specialize (forall_u _ Hu).
    eapply type_Cumul_alt.
    econstructor; eauto.
    eapply type_Cumul_alt. eauto. s1; auto.
    apply: red_cumul Hu.
    unshelve eapply (closed_context_conversion _ typeb').
    constructor; pcuic.
    eapply type_Cumul_alt. eauto. pcuic. apply: red_cumul Hu.
    constructor; auto. eapply ws_cumul_ctx_pb_refl; eauto. constructor; auto.
    eapply ws_cumul_pb_refl; eauto; repeat inv_on_free_vars =>//.
    apply: red_conv Hu.
    assert (Σ ;;; Γ |- tLetIn n b b_ty b' : tLetIn n b b_ty b'_ty). econstructor; eauto.
    eapply (validity X0).
    eapply cumul_red_r.
    apply cumul_refl'. constructor. apply Hu.

  -
    eapply substitution0; eauto.
    pose proof typet as typet'.
    eapply inversion_Lambda in typet' as [s1 [B' [Ht [Hb HU]]]]=>//.
    apply cumul_Prod_inv in HU as [eqann eqA leqB] ⇒ //.
    pose proof (validity typet) as i.
    eapply isType_tProd in i as [Hdom Hcodom]; auto.
    eapply type_ws_cumul_pb; eauto.
    unshelve eapply (closed_context_conversion _ Hb); pcuics.
    constructor. now apply ws_cumul_ctx_pb_refl. constructor; auto.

  -
    assert (args []) by (destruct args; simpl in *; congruence).
    symmetry in H3. apply tApp_mkApps_inj in H3 as [-> Hu]; auto.
    rewrite mkApps_nonempty; auto.
    epose (last_nonempty_eq H4). rewrite <- Hu in e. rewrite <- e.
    clear e.
    specialize (inversion_mkApps typet) as [T' [appty spty]].
    have vT' := (validity appty).
    eapply type_tFix_inv in appty as [T [arg [fn' [[[Hnth wffix] Hty]]]]]; auto.
    rewrite H in Hnth. noconf Hnth.
    eapply type_App; eauto.
    eapply type_mkApps; [|tea].
    eapply type_ws_cumul_pb; eauto.

  -
    intuition auto.
    eapply type_Cumul_alt; [eapply type_App| |]; eauto with wf.
    eapply validity.
    eapply type_App; eauto. eapply red_cumul_inv.
    eapply (@red_red _ _ wf _ Γ [vass na A] [] [u] [N2]); eauto.
    erewriteon_free_vars_ctx_on_ctx_free_vars.
    eapply on_free_vars_ctx_snoc_ass; tea.
    eapply type_closed in typeu. now eapply closedn_on_free_vars.
    eapply type_closed in typet. cbn in typet; repeat inv_on_free_vars.
    cbn. now eapply closedn_on_free_vars. constructor. apply: red1_red Hu. constructor.
    all:repeat constructor. cbn.
    rewrite -(shiftnP_add 1) addnP_shiftnP. repeat inv_on_free_vars ⇒ //.

  -
    unshelve epose proof (declared_constant_inj decl decl0 _ _); tea; subst decl.
    destruct decl0 as [ty body' univs]; simpl in *; subst body'.
    eapply on_declared_constant in H; tas; cbn in H.
    rewrite <- (app_context_nil_l Γ).
    apply subject_closed in H as clb; tas.
    apply type_closed in H as clty; tas.
    replace (subst_instance u body)
      with (lift0 #|Γ| (subst_instance u body)).
    replace (subst_instance u ty)
      with (lift0 #|Γ| (subst_instance u ty)).
    2-3: rewrite -subst_instance_lift lift_closed; cbnr; tas.
    eapply weakening; tea.
    now rewrite app_context_nil_l.
    eapply @typing_subst_instance_decl with (Γ:=[]); tea.

  -
    clear forall_u forall_u0 X X0.
    destruct X4 as [wfcpc IHcpc].
    eassert (ctx_inst _ _ _ _) as Hctxi by (eapply ctx_inst_impl with (2 := X5); now intros ? []).
    eassert (PCUICEnvTyping.ctx_inst _ _ _ _ _) as IHctxi.
    { eapply ctx_inst_impl with (2 := X5). intros ? ? ? ? [? r]; exact r. }
    hide X8.
    pose proof typec as typec''.
    unfold iota_red.
    pose proof typec as typec'.
    eapply inversion_mkApps in typec as [A [tyc tyargs]]; auto.
    eapply (inversion_Construct Σ wf) in tyc as [mdecl' [idecl' [cdecl [wfl [declc [Hu tyc]]]]]].
    eapply typing_spine_strengthen in tyargs; tea.
    have openargs : forallb (is_open_term Γ) args.
    { repeat inv_on_free_vars; auto. }
    clear tyc.
    2:{ eapply validity. econstructor; tea. }
    unshelve eapply Construct_Ind_ind_eq in typec'; eauto.
    pose proof (declared_inductive_inj isdecl (proj1 declc)) as [-> ->].
    destruct typec' as [[[[[_ equ] cu] cu'] eqargs] [cparsubst [cargsubst [iparsubst [iidxsubst ci']]]]].
    destruct ci' as [cparsubst0 iparsubst0 idxsubst0 subsidx [s [typectx [Hpars Hargs]]]].
    pose proof (on_declared_constructor declc) as [[onind oib] [ctor_sorts [hnth onc]]].
    unshelve epose proof (constructor_cumulative_indices declc Hu cu' equ _ _ _ _ _ cparsubst0 iparsubst0 Hpars).
    set (argctxu1 := subst_context _ _ _) in X |- ×.
    set (argctxu := subst_context _ _ _) in X |- ×.
    simpl in X.
    set (pargctxu1 := subst_context cparsubst 0 argctxu1) in X |- ×.
    set (pargctxu := subst_context iparsubst 0 argctxu) in X |- ×.
    destruct X as [cumargs convidx]; eauto.
    assert(wfparu : wf_local Σ (subst_instance (puinst p) (ind_params mdecl))).
    { eapply on_minductive_wf_params; eauto. }
    assert (wfps : wf_universe Σ ps).
    { eapply validity in IHp; auto. eapply PCUICWfUniverses.isType_wf_universes in IHp; tea.
      now apply (ssrbool.elimT PCUICWfUniverses.wf_universe_reflect) in IHp. }
    have lenpars := (wf_predicate_length_pars H0).
    unfold hidebody in X8.
    set (ptm := it_mkLambda_or_LetIn _ _).
    rename c0 into c.
    assert (isType Σ Γ (mkApps ptm (indices ++ [mkApps (tConstruct ci c u) args]))).
    { eapply validity. econstructor; eauto. all :constructor; eauto. apply (All2i_impl X8). intuition auto. }
    eapply All2i_nth_error in X8; tea.
    2:{ destruct declc. simpl in e. exact e. }
    cbn in X8.
    destruct X8 as (bctxeq & (wfcbc & _) & (hb & _) & cbty & _).
    cbn -[case_branch_type_gen] in hb.
    rewrite case_branch_type_fst in hb.
    set (prebrctx := pre_case_branch_context ci mdecl (pparams p) (puinst p) cdecl).
    set (ibrctx := (case_branch_context ci mdecl p (forget_types (bcontext br)) cdecl)) in ×.
    set (brctx := (inst_case_context (pparams p) (puinst p) (bcontext br))).
    assert (wfbr : wf_branch cdecl br).
    { eapply Forall2_All2, All2_nth_error in H4; tea.
      eapply declc. }
    assert(eqctx : eq_context_upto_names ibrctx brctx).
    { rewrite /brctx /ibrctx.
      rewrite /case_branch_context /case_branch_context_gen.
      etransitivity.
      eapply eq_binder_annots_eq.
      eapply wf_pre_case_branch_context_gen; tea.
      unfold pre_case_branch_context_gen.
      rewrite /inst_case_context.
      now eapply alpha_eq_subst_context, alpha_eq_subst_instance. }
    assert (convbrctx' : Σ Γ ,,, brctx = Γ ,,, ibrctx).
    { etransitivity; tea.
      eapply ws_cumul_ctx_pb_app; revgoals.
      3:eapply ws_cumul_ctx_pb_refl; eapply wf_local_closed_context; auto.
      split. apply ws_cumul_ctx_pb_refl. pcuic.
      eapply eq_context_alpha_conv ⇒ //. now symmetry.
      eapply wf_local_closed_context. eapply typing_wf_local in hb.
      eapply wf_local_alpha; tea. eapply All2_app ⇒ //. reflexivity.
      now apply typing_wf_local, wf_local_closed_context in hb.
      rewrite /brctx /ibrctx; len.
      rewrite case_branch_context_length //. }
    assert (convbrctx'' : Σ Γ ,,, ibrctx = Γ ,,, prebrctx).
    { rewrite /ibrctx /prebrctx.
      symmetry.
      apply ws_cumul_ctx_pb_rel_app.
      eapply eq_context_alpha_conv.
      eapply pre_case_branch_context_eq; tea.
      eapply wf_local_closed_context. eapply wf_pre_case_branch_context; tea.
      now apply typing_wf_local, wf_local_closed_context in cbty. }
    assert (prewf : wf_local Σ (Γ ,,, prebrctx)).
    { eapply wf_pre_case_branch_context; tea. }
    assert (prewfs : wf_local Σ (Γ ,,, smash_context [] prebrctx)).
    { eapply wf_local_smash_end; tea. }
    assert (wfbrctx' : wf_local Σ (Γ ,,, brctx)).
    { eapply wf_local_alpha. eapply All2_app; tea. eapply All2_refl; reflexivity. assumption. }
    assert (convbrctxsmash : Σ
        Γ ,,, smash_context [] (case_branch_context ci mdecl p (forget_types (bcontext br)) cdecl) =
        Γ ,,, smash_context [] brctx).
    { eapply conv_context_smash_end; tea. now symmetry. }
    assert (spbrctx : spine_subst Σ Γ (skipn (ind_npars mdecl) args) (List.rev (skipn (ind_npars mdecl) args))
      (smash_context [] prebrctx)).
    { pose proof (spine_subst_smash idxsubst0).
      eapply spine_subst_cumul in X0. eapply X0. all:tea.
      1-2:apply smash_context_assumption_context; pcuic.
      eapply X0.
      move: cumargs.
      rewrite /pargctxu /argctxu.
      move: iparsubst0.
      rewrite (firstn_app_left).
      now rewrite (wf_predicate_length_pars H0).
      intros iparsubst0.
      clear X5 IHctxi. unshelve epose proof (ctx_inst_spine_subst _ Hctxi).
      eapply weaken_wf_local; tea. exact (on_minductive_wf_params_indices_inst isdecl _ cu').
      rewrite (spine_subst_inst_subst iparsubst0).
      intros cum.
      eapply ws_cumul_ctx_pb_rel_trans; tea.
      apply ws_cumul_ctx_pb_rel_app.
      apply ws_cumul_ctx_pb_refl.
      now apply wf_local_closed_context in prewfs. }
    eapply closed_context_conversion in hb.
    3:{ symmetry. eapply convbrctx'. }
    eapply typing_expand_lets in hb.
    eapply (PCUICSubstitution.substitution (Δ := [])) in hb.
    2:{ eapply (spine_subst_cumul (Γ' := smash_context [] brctx)) in spbrctx; tea.
        eapply spbrctx.
        1-2:apply smash_context_assumption_context; pcuic.
        now apply wf_local_smash_end.
        apply ws_cumul_ctx_pb_rel_smash ⇒ //.
        apply ws_cumul_ctx_pb_rel_app. apply ws_cumul_ctx_pb_eq_le. symmetry.
        etransitivity; tea. }
    rewrite subst_context_nil -heq_ind_npars in hb ×.
    eapply (type_ws_cumul_pb (pb:=Cumul)). exact hb. 3:auto.
    assumption. clear hb.
    rewrite /case_branch_type.
    set cbtyg := (case_branch_type_gen _ _ _ _ _ _ _ _ _).
    transitivity (subst0 (List.rev (skipn (ind_npars mdecl) args)) (expand_lets prebrctx cbtyg.2)).
    { eapply ws_cumul_pb_eq_le.
      eapply (substitution_ws_cumul_pb (Γ'' := [])). eapply spbrctx.
      symmetry. apply (ws_cumul_pb_expand_lets_ws_cumul_ctx (pb:=Cumul)); tea.
      eapply wt_cumul_pb_refl.
      rewrite case_branch_type_fst in cbty.
      eapply closed_context_conversion in cbty. exact cbty.
      auto. auto.
      eapply ws_cumul_ctx_pb_rel_app; tea. eapply ws_cumul_ctx_pb_eq_le.
      symmetry. now transitivity (Γ ,,, ibrctx). }
    cbn.
    rewrite lift_mkApps !subst_mkApps.
    pose proof (wf_branch_length wfbr).
    have lenskip: #|skipn (ind_npars mdecl) args| = (context_assumptions (cstr_args cdecl)).
    { rewrite List.skipn_length eqargs; lia. }
    have lenfirst: #|firstn (ind_npars mdecl) args| = (context_assumptions (ind_params mdecl)).
    { rewrite firstn_length_le; try lia. now rewrite -(declared_minductive_ind_npars isdecl). }
    have brctxlen : #|prebrctx| = #|cstr_args cdecl|.
    { now rewrite /prebrctx !lengths. }
    have pparamsl : #|pparams p| = context_assumptions (ind_params mdecl).
    { move: (wf_predicate_length_pars H0).
      now rewrite (declared_minductive_ind_npars isdecl). }

    rewrite simpl_lift; try lia.
    rewrite subst_subst_lift // !lengths //; try lia.
    rewrite map_app /= !map_app. eapply ws_cumul_pb_eq_le.
    have wfparsargs : wf_local Σ
      (subst_instance u (ind_params mdecl),,,
        subst_context (inds (inductive_mind ci) u (ind_bodies mdecl))
          #|ind_params mdecl| (subst_instance u (cstr_args cdecl))).
    { exact (on_constructor_wf_args declc Hu). }
    have wfparsargs' : wf_local Σ
      (subst_instance (puinst p) (ind_params mdecl),,,
        subst_context (inds (inductive_mind ci) (puinst p) (ind_bodies mdecl))
          #|ind_params mdecl| (subst_instance (puinst p) (cstr_args cdecl))).
    { exact (on_constructor_wf_args declc cu'). }
    eapply ws_cumul_pb_mkApps; tea.
    { eapply wt_cumul_pb_refl. eapply type_it_mkLambda_or_LetIn; tea. }
    rewrite firstn_app_left // /= in iparsubst0.
    rewrite firstn_app_left // /= in Hpars.
    rewrite skipn_all_app_eq // in subsidx.
    have brctxass : context_assumptions prebrctx = context_assumptions (cstr_args cdecl).
    { now rewrite /prebrctx !lengths. }
    assert (eqargts : ws_cumul_pb_terms Σ Γ (skipn (ind_npars mdecl) args)
      (skipn (ind_npars mdecl) args)).
    { pose proof (spine_subst_ctx_inst spbrctx).
      apply ctx_inst_open_terms in X0.
      eapply All_All2; tea. cbn; intros.
      apply ws_cumul_pb_refl; tea. }
      
    eapply All2_app.
    × set(indsub := inds _ _ _).
      relativize (map (subst0 _) _).
      2:{
        rewrite !map_map_compose. apply map_extx.
        symmetry.
        rewrite -/(subst_let_expand _ _ _) -/(subst_let_expand_k _ _ _ _).
        rewrite -brctxass -brctxlen -expand_lets_eq.
        rewrite {1 2}/prebrctx {1 2}/pre_case_branch_context {1}subst_context_length.
        rewrite /subst_let_expand_k (expand_lets_subst_comm _ _ _) !lengths.
        relativize (context_assumptions _).
        erewrite <- subst_app_simpl. 2:now rewrite !lengths.
        rewrite subst_app_decomp.
        relativize #|cstr_args cdecl|.
        erewrite subst_let_expand_app.
        2-4:rewrite ?lengths; try lia; reflexivity.
        rewrite /subst_let_expand.
        reflexivity. }
      move: Hargs.
      move: convidx.
      intros cv convidx.
      eapply (ws_cumul_pb_terms_subst (Δ := [])) in cv.
      3:{ exact (spine_subst_smash idxsubst0). }
      3:{ exact (spine_subst_smash idxsubst0). }
      all:tea. 2:{ eapply wf_local_closed_context. eapply wf_local_smash_end; tea. eapply idxsubst0. }
      2:{ eapply All2_rev ⇒ //. }
      rewrite subst_context_nil /= in cv. simpl in cv.
      rewrite skipn_all_app_eq // in convidx.

      assert(ws_cumul_pb_terms Σ Γ
        (map
         (fun x : term
          subst0 (List.rev args)
            (expand_lets (argctxu1 ++ subst_instance u (ind_params mdecl)) (subst_instance u x)))
          (cstr_indices cdecl)) indices).
      { eapply eq_ws_cumul_pb_terms_trans; tea.
        pose proof (positive_cstr_closed_indices declc).
        eapply All_map_inv in X0.
        eapply All_map_eq, All_impl; tea.
        cbn; intros x.
        intros cl.
        epose proof
          ( @spine_subst_app _ Σ Γ (subst_instance u (ind_params mdecl))
            (subst_context
              (inds (inductive_mind ci) u (ind_bodies mdecl))
               #|ind_params mdecl| (subst_instance u (cstr_args cdecl)))
          (firstn (ind_npars mdecl) args)
          (skipn (ind_npars mdecl) args) (cargsubst ++ cparsubst)) as X3.
        rewrite lenfirst in X3. len in X3.
        specialize (X3 eq_refl).
        forward X3. { rewrite -app_context_assoc. eapply weaken_wf_local; tea. }
        forward X3. {
          rewrite skipn_all_app_eq; len.
          now rewrite -(PCUICContextSubst.context_subst_length idxsubst0); len.
          apply cparsubst0. }
        forward X3. {
          pose proof (PCUICContextSubst.context_subst_length idxsubst0).
          len in H8.
          rewrite firstn_app H8 firstn_all Nat.sub_diag /= app_nil_r skipn_all_app_eq //. }
        rewrite firstn_skipn in X3.
        rewrite (spine_subst_inst_subst_term X3).
        f_equal.
        pose proof (PCUICInductiveInversion.on_constructor_wf_args declc).
        eapply closed_wf_local in X4; tea.
        rewrite !closedn_ctx_app /= in X4 ×.
        move/andb_and: X4 ⇒ [] /andb_and [] clar clp clargs.
        len in clargs.
        rewrite -(subst_closedn (inds (inductive_mind ci) u (ind_bodies mdecl))
              (context_assumptions (ind_params mdecl ,,, cstr_args cdecl))
              (expand_lets _ _)).
        { rewrite /argctxu1.
          relativize (context_assumptions _).
          eapply (closedn_expand_lets 0).
          rewrite !closedn_ctx_app /=.
          apply andb_true_iff; split.
          rewrite closedn_subst_instance_context.
          eapply (declared_inductive_closed_params isdecl).
          rewrite subst_instance_length.
          eapply (closedn_ctx_subst 0). simpl.
          rewrite /ind_subst inds_length.
          now rewrite closedn_subst_instance_context.
          eapply (declared_minductive_closed_inds isdecl).
          rewrite /= app_length subst_context_length !subst_instance_length.
          rewrite Nat.add_comm in cl.
          eapply (PCUICClosed.closedn_expand_lets) in cl.
          rewrite closedn_subst_instance.
          now rewrite Nat.add_comm.
          rewrite /= !context_assumptions_app /= context_assumptions_subst_context //
            !context_assumptions_subst_instance //. }
        
        relativize (context_assumptions _).
        erewrite <-(expand_lets_subst_comm _ _ _).
        2:{ now rewrite /argctxu1 !context_assumptions_app
              !context_assumptions_subst_context !context_assumptions_subst_instance. }
        f_equal.
        × rewrite subst_context_app closed_ctx_subst.
          rewrite closedn_subst_instance_context.
          now apply (declared_inductive_closed_params isdecl).
          f_equal. len.
          rewrite closed_ctx_subst //.
          rewrite /argctxu1. simpl.
          eapply (closedn_ctx_subst 0). simpl.
          rewrite /ind_subst inds_length closedn_subst_instance_context //.
          eapply (declared_minductive_closed_inds isdecl).
        × now rewrite /argctxu1; len. }
      clear convidx.
      etransitivity; tea.
      eapply (eq_ws_cumul_pb_terms_trans (U:=
       (map (subst0 (List.rev (skipn (ind_npars mdecl) args)))
      (map (subst iparsubst (context_assumptions (cstr_args cdecl)))
         (map (expand_lets argctxu)
            (map (subst_instance (puinst p)) (cstr_indices cdecl))))))).
      2:{
        rewrite !map_map_compose.
        rewrite !map_map_compose in cv.
        eapply All2_map_inv, All2_All in cv.
        eapply All2_map, All_All2; tea.
        cbn; intros x Hx.
        eapply ws_cumul_pb_eq_trans.
        symmetry; tea.
        rewrite (spine_subst_inst_subst_term_k cparsubst0).
        pose proof (subst_let_expand_app).
        relativize (context_assumptions (cstr_args cdecl)).
        erewrite <-subst_app_simpl. 2:now len.
        rewrite -List.rev_app_distr firstn_skipn. len.
        rewrite lenskip expand_lets_app /argctxu1.
        rewrite context_assumptions_subst_context context_assumptions_subst_instance //. }
  
      
      rewrite /argctxu. simpl.
      rewrite !map_map_compose. apply All_map_eq.
      eapply All_impl.
      exact (All_map_inv _ _ _ (positive_cstr_closed_indices declc)).
      cbnx.
      rewrite -(closed_ctx_subst indsub 0 (subst_instance _ _ ,,, _)).
      { now eapply closed_wf_local in wfparsargs'. }
      relativize (#|ind_params _| + _).
      erewrite expand_lets_subst_comm; rewrite !lengths.
      2:rewrite !lengths; lia.
      rewrite -context_assumptions_app Nat.add_comm.
      move/(PCUICClosed.closedn_expand_lets) ⇒ /=. rewrite /= !lengthsclx.
      rewrite (subst_closedn indsub (_ + _)).
      relativize (_ + _). eapply (closedn_expand_lets 0).
      2-3:rewrite /= !lengths // closedn_subst_instance //.
      eapply closed_wf_local; tea. now rewrite Nat.add_comm.
      rewrite (spine_subst_inst_subst_term_k iparsubst0).
      change (ind_subst _ _ _) with indsub.
      relativize (context_assumptions _).
      erewrite <-subst_app_simpl. 2:now len.
      rewrite List.rev_length lenskip /=.
      relativize (context_assumptions _).
      erewrite <- expand_lets_app ⇒ //.
      now rewrite !lengths.

    × rewrite lift_mkApps /= !subst_mkApps /=. constructor. 2:constructor.
      rewrite !map_app.
      rewrite -{3}(firstn_skipn (ind_npars mdecl) args) -brctxlen -brctxass.
      rewrite - !expand_lets_eq_map.
      rewrite -/(expand_lets_k (bcontext br) 0 _).
      relativize (to_extended_list (cstr_args cdecl)).
      erewrite map_expand_lets_to_extended_list.
      2:{ etransitivity.
        2:apply to_extended_list_case_branch_context.
        rewrite /prebrctx.
        eapply conv_context_rel_to_extended_list.
        apply ws_cumul_ctx_pb_rel_app. symmetry. tea.
        now eapply Forall2_All2 in wfbr. }
      rewrite -map_expand_lets_to_extended_list.
      rewrite !map_map_compose.
      rewrite [map (fun x_) (to_extended_list _)](@map_subst_let_expand_to_extended_list _ Σ _ Γ); tea.
      relativize (map _ _).
      2:{ eapply map_extx. rewrite -/(subst_let_expand _ _ _).
          now rewrite subst_let_expand_lift_id //; len. }
      rewrite map_id.
      transitivity (mkApps (tConstruct ci c (puinst p)) args).
      rewrite -(firstn_skipn (ind_npars mdecl) args).
      eapply ws_cumul_pb_mkApps; tea.
      eapply ws_cumul_pb_refl ⇒ //.
      eapply All2_app. eapply All2_symP ⇒ //. intro; now symmetry.
      rewrite firstn_skipn //.
      rewrite firstn_skipn. constructor ⇒ //.
      { rewrite on_free_vars_mkApps /= //. }
      { rewrite on_free_vars_mkApps /= //. }
      eapply eq_term_upto_univ_mkApps.
      2:reflexivity.
      constructor. eapply R_global_instance_sym; tc.
      rewrite eqargs.
      now eapply (R_global_instance_cstr_irrelevant declc).

  -
    eapply inversion_mkApps in typec as [? [tcof ?]] ⇒ //.
    eapply type_tCoFix_inv in tcof as [d [[[Hnth wfcofix] ?] ?]] ⇒ //.
    unfold unfold_cofix in H.
    rewrite Hnth in H. noconf H.
    pose proof (validity t0).
    eapply typing_spine_strengthen in t; eauto.
    eapply wf_cofixpoint_typing_spine in t; eauto.
    unfold check_recursivity_kind in t.
    rewrite isdecl.p1 in t.
    apply ReflectEq.eqb_eq in t. rewrite t /= in heq_isCoFinite.
    discriminate.

  -
    eassert (ctx_inst _ _ _ _) as Hctxi by (eapply ctx_inst_impl with (2 := X5); now intros ? []).
    eassert (PCUICEnvTyping.ctx_inst _ _ _ _ _) as X6.
    { eapply ctx_inst_impl with (2 := X5). intros ? ? ? ? [? r]; exact r. }
    clear X5; rename Hctxi into X5.
    destruct X0, X4.
    assert (isType Σ Γ (mkApps (it_mkLambda_or_LetIn (case_predicate_context ci mdecl idecl p) (preturn p)) (indices ++ [c]))).
    { eapply validity. econstructor; eauto. all: econstructor; eauto.
      eapply (All2i_impl X8); intuition auto. }
    set (ptm := it_mkLambda_or_LetIn _ _) in ×.
    cbn -[ptm it_mkLambda_or_LetIn] in ×.
    have wfparinds : wf_local Σ
      (Γ,,, subst_instance (puinst p) (ind_params mdecl,,, ind_indices idecl)).
    { eapply weaken_wf_local; tea.
      eapply (on_minductive_wf_params_indices_inst isdecl _ H1). }
    have ctxi' : ctx_inst Σ Γ (params' ++ indices)
        (List.rev
           (subst_instance p.(puinst) (ind_params mdecl,,, ind_indices idecl))).
    { eapply OnOne2_prod_inv in X3 as [X3 _].
      eapply OnOne2_app_r in X3.
      unshelve eapply (ctx_inst_merge' _ _ _ _ _ X6 X5); tea. }
    pose proof X5 as X5'.
    unshelve epose proof (ctx_inst_spine_subst _ X5); tea.
    eapply spine_subst_smash in X4; tea.
    eapply ctx_inst_length in X5. len in X5.
    rewrite context_assumptions_rev in X5. len in X5.
    pose proof (wf_predicate_length_pars H0). simpl in H.
    pose proof (declared_minductive_ind_npars isdecl).
    have lenidx : (#|List.rev indices| = (context_assumptions (ind_indices idecl))) by (len; lia).
    rewrite subst_instance_app smash_context_app_expand in X4.
    eapply spine_subst_app_inv in X4 as [sppars spargs]; tea. 2:len.
    len in sppars. len in spargs.
    rewrite List.rev_app_distr in sppars spargs.
    rewrite skipn_app - !lenidx !skipn_all /= Nat.sub_diag skipn_0 in sppars spargs.
    rewrite firstn_app firstn_all Nat.sub_diag /= app_nil_r in spargs.
    rewrite subst_instance_app List.rev_app_distr in X6.
    have lenpars' := (OnOne2_length X3).
    unshelve epose proof (ctx_inst_spine_subst _ ctxi');tea.
    pose proof (spine_codom_wf _ _ _ _ _ X4);tea.
    pose proof (spine_subst_smash X4); tea. all:tea.
    rewrite subst_instance_app smash_context_app_expand in X9.
    eapply spine_subst_app_inv in X9 as [sppars' spargs']; tea.
    2:len. len in sppars'. len in spargs'.
    rewrite List.rev_app_distr in sppars' spargs'.
    rewrite skipn_app - !lenidx !skipn_all /= Nat.sub_diag skipn_0 in sppars' spargs'.
    rewrite firstn_app firstn_all Nat.sub_diag /= app_nil_r in spargs'.
    have wfp' : wf_predicate mdecl idecl (set_pparams p params').
    { move: H0. rewrite /wf_predicate /wf_predicate_gen /=.
      rewrite (OnOne2_length X3). intuition auto. }
    have redpars : red_terms Σ Γ (pparams p) params'.
    { eapply OnOne2_prod_inv in X3 as [cv _].
      clear -cv H H3. inv_on_free_vars.
      cbn in *; repeat inv_on_free_vars. clear b a2 a1 a0.
      induction cv; cbn; constructor; auto using closed_red1_red;
      cbn in *; repeat inv_on_free_vars; auto.
      apply red_terms_refl ⇒ //. now apply into_closed_red. }
    have convctx' :
      Σ (case_predicate_context ci mdecl idecl p ++ Γ) =
      (case_predicate_context ci mdecl idecl (set_pparams p params') ++ Γ).
    { move: X2cv.
      rewrite /case_predicate_context /case_predicate_context_gen.
      eapply ws_cumul_ctx_pb_rel_app.
      eapply conv_ctx_set_binder_name.
      { change (pcontext (set_pparams p params')) with (pcontext p).
        eapply wf_pre_case_predicate_context_gen; tea. }
      { now eapply wf_pre_case_predicate_context_gen. }
      rewrite /pre_case_predicate_context_gen /inst_case_context.
      cbn [pparams puinst set_pparams].
      eapply ws_cumul_ctx_pb_rel_app.
      eapply substitution_ws_cumul_ctx_pb_red_subst.
      3:eapply subslet_untyped_subslet, sppars.
      2:eapply All2_rev ⇒ //.
      clear cv.
      rewrite -app_context_assoc. eapply is_closed_context_weaken. fvs.
      rewrite -on_free_vars_ctx_on_ctx_free_vars -closedP_shiftnP_eq
       -closed_ctx_on_ctx_free_vars.
      rewrite closedn_ctx_app !lengths.
      apply/andP; split. 2:cbn -[ind_predicate_context].
      2:rewrite closedn_subst_instance_context. 2:eapply closed_ind_predicate_context; tea.
      2:eapply declared_minductive_closed, isdecl.
      eapply closedn_smash_context.
      now eapply declared_inductive_closed_params_inst. }
    have isty' : isType Σ Γ (mkApps (tInd ci (puinst p)) (params' ++ indices)).
    { eexists; eapply isType_mkApps_Ind; tea. }
    have wfcpc' : wf_local Σ (Γ ,,, case_predicate_context ci mdecl idecl (set_pparams p params')).
    { eapply wf_case_predicate_context; tea. }
    have eqindices : ws_cumul_pb_terms Σ Γ indices indices.
    { now eapply spine_subst_wt_terms, wt_terms_ws_cumul_pb in spargs'. }
    have typec' : Σ;;; Γ |- c : mkApps (tInd ci (puinst p)) (params' ++ indices).
    { eapply type_ws_cumul_pb; tea.
      eapply ws_cumul_pb_eq_le. eapply ws_cumul_pb_mkApps; pcuic.
      eapply All2_app ⇒ //. now apply: red_terms_ws_cumul_pb_terms. }
    set (pctx := (inst_case_predicate_context (set_pparams p params'))) in ×.
    pose proof (snd (All2_fold_All2 _) X1). symmetry in X9. move:X9.
    change (pcontext p) with (pcontext (set_pparams p params')).
    move/(PCUICAlpha.inst_case_predicate_context_eq wfp') ⇒ eqctx.
    have wfpctx : wf_local Σ (Γ,,, inst_case_predicate_context (set_pparams p params')).
    { eapply wf_local_alpha; tea; auto.
      eapply All2_app ⇒ //.
      now eapply All2_fold_All2 in eqctx.
      eapply All2_refl; reflexivity. }
    have eqpctx : Σ Γ ,,, pctx = Γ ,,, case_predicate_context ci mdecl idecl (set_pparams p params').
    { symmetry.
      rewrite /pctx.
      eapply into_ws_cumul_ctx_pb ⇒ //.
      now eapply wf_local_closed_context.
      now eapply wf_local_closed_context.
      eapply upto_names_conv_context.
      eapply eq_context_upto_cat. apply eq_context_upto_refl; tc.
      now apply eq_context_gen_upto. }
    epose proof (wf_case_branches_types' (p:=set_pparams p params') ps _ brs isdecl isty' wfp').
    cbv zeta in X9; forward_keep X9.
    { eapply closed_context_conversion; tea. }
    do 2 forward X9 by auto.
    eapply type_ws_cumul_pb; tea.
    { econstructor; tea. all: econstructor; tea.
      apply All2i_nth_hyp in X9.
      eapply All2i_All2i_mix in X8; tea. clear X9.
      eapply (All2i_impl X8); clear X8.
      intros cstr cdecl br. cbv zeta.
      rewrite !case_branch_type_fst.
      do 2 case. movehnth [] wfbr wfbctxargs wfbrctx wfcbc' wfcbcty'.
      caseeqbctx. case. casewfbctx _.
      move⇒ [] [] Hbody IHbody [] brty IHbrty.
      eapply conj_impl. solve_all. movecvcbc.
      apply conj_impl; [|movewfcb'].
      { now eapply typing_wf_local in wfcbcty'. }
      split ⇒ //.
      have declc : declared_constructor Σ (ci, cstr) mdecl idecl cdecl.
      { split ⇒ //. }
      have convbctx : Σ Γ,,, case_branch_context ci mdecl p (forget_types (bcontext br)) cdecl =
        Γ,,, case_branch_context ci mdecl (set_pparams p params') (forget_types (bcontext br)) cdecl.
      { rewrite /case_branch_context /case_branch_context_gen.
        eapply ws_cumul_ctx_pb_rel_app.
        eapply conv_ctx_set_binder_name. eapply wf_pre_case_branch_context_gen; tea.
        eapply wf_pre_case_branch_context_gen; tea.
        rewrite /case_branch_context /case_branch_context_gen.
        eapply (substitution_ws_cumul_ctx_pb_subst_conv (Γ' := smash_context [] (ind_params mdecl)@[puinst p]) (Γ'':=[])).
        2:{ eapply All2_rev.
          eapply OnOne2_prod_inv in X3 as [redp _].
          now eapply red_terms_ws_cumul_pb_terms. }
        apply ws_cumul_ctx_pb_rel_app.
        eapply ws_cumul_ctx_pb_refl, wf_local_closed_context.
        rewrite /=. rewrite /cstr_branch_context.
        rewrite subst_instance_expand_lets_ctx.
        eapply wf_local_expand_lets.
        epose proof (on_constructor_inst_wf_args declc (puinst p) H1) as onc.
        rewrite -app_context_assoc; eapply weaken_wf_local; auto.
        rewrite subst_instance_subst_context.
        now rewrite subst_instance_inds (subst_instance_id_mdecl _ _ _ H1).
        eapply subslet_untyped_subslet, sppars. eapply subslet_untyped_subslet, sppars'.
        eapply wf_local_closed_context.
        eapply wf_local_smash_end.
        apply weaken_wf_local ⇒ //. eapply on_minductive_wf_params; tea. eapply isdecl. }
      eapply (type_ws_cumul_pb (pb:=Conv)); tea.
      + eapply closed_context_conversion; tea.
      + ps. exact wfcbcty'.
      + eapply ws_cumul_pb_mkApps; tea.
        { rewrite /ptm. cbn [preturn set_pparams].
          rewrite !lift_it_mkLambda_or_LetIn.
          eapply ws_cumul_pb_it_mkLambda_or_LetIn.
          relativize #|cstr_args cdecl|.
          eapply weakening_ws_cumul_ctx_pb; tea.
          apply ws_cumul_ctx_pb_refl, wf_local_closed_context ⇒ //.
          now apply (case_branch_context_length_args wfbr).
          rewrite !case_predicate_context_length // /= Nat.add_0_r.
          relativize #|pcontext p|. relativize #|cstr_args cdecl|.
          eapply weakening_ws_cumul_pb; tea.
          apply isType_ws_cumul_pb_refl. now ps.
          now apply wf_local_closed_context.
          now apply case_branch_context_length_args.
          now rewrite case_predicate_context_length. }
        cbn.
        eapply All2_app.
        - rewrite /case_branch_context /case_branch_context_gen /pre_case_branch_context
          /pre_case_branch_context_gen /inst_case_context. cbn.
          symmetry. rewrite /subst_context PCUICRenameConv.map2_set_binder_name_fold ?lengths.
          now apply wf_branch_length.
          rewrite -/(subst_context _ _ _).
          relativize #|cstr_args cdecl|.
          eapply ws_cumul_pb_terms_subst.
          2:eapply subslet_untyped_subslet, sppars'.
          2:eapply subslet_untyped_subslet, sppars.
          { eapply wf_local_closed_context, wf_local_smash_end, weaken_wf_local ⇒ //.
            eapply (on_minductive_wf_params isdecl) ⇒ //. }
          { apply All2_rev; symmetry. now apply red_terms_ws_cumul_pb_terms. }
          { epose proof (on_constructor_closed_indices_inst declc (u:=puinst p) H1).
            eapply ws_cumul_pb_terms_refl.
            { rewrite /cstr_branch_context.
              apply wf_local_closed_context.
              move: wfbrctx.
              move/wf_local_expand_lets. cbn.
              rewrite subst_instance_expand_lets_ctx map2_set_binder_name_expand_lets ?lengths //.
              apply (wf_branch_length wfbr).
              rewrite subst_instance_subst_context instantiate_inds //.
              eapply declc. }
            rewrite 2!forallb_map.
            eapply All_map_inv in X8. eapply All_forallb, All_impl; tea.
            cbn; intros x clx.
            apply closedn_on_free_vars.
            rewrite -on_free_vars_closedn in clx.
            len. rewrite !map2_length !lengths.
            now apply wf_branch_length. rewrite lengths in clx.
            rewrite (wf_branch_length wfbr).
            rewrite (Nat.add_comm _ #|Γ|) Nat.add_assoc (Nat.add_comm _ #|Γ|).
            rewrite -(context_assumptions_subst_instance (puinst p)) closedn_expand_lets_eq.
            eapply closedn_ctx_upwards. eapply (declared_inductive_closed_params_inst declc). lia.
            len. rewrite (Nat.add_comm #|ind_params mdecl|).
            eapply closed_upwards; tea. len. }
          pose proof (wf_branch_length wfbr).
          now rewrite map2_length !lengths.
        - apply All2_tip, ws_cumul_pb_mkApps; [apply into_ws_cumul_pb ⇒ //; try reflexivity|].
          now eapply wf_local_closed_context.
          eapply All2_app. eapply All2_map.
          eapply OnOne2_prod_inv in X3 as [X3 _].
          eapply red_terms_ws_cumul_pb_terms in redpars.
    &nb