Library MetaCoq.PCUIC.PCUICExpandLetsCorrectness

From Coq Require Import ssreflect ssrbool Utf8 CRelationClasses.
From Equations.Type Require Import Relation Relation_Properties.
Require Import Equations.Prop.DepElim.
From Equations Require Import Equations.

Set Warnings "-notation-overridden".
From MetaCoq.Template Require Import config utils.
From MetaCoq.PCUIC Require Import PCUICAst PCUICAstUtils PCUICOnOne PCUICCases PCUICInduction
     PCUICLiftSubst PCUICEquality PCUICReduction PCUICCasesContexts PCUICTactics
     PCUICSigmaCalculus PCUICClosed PCUICClosedTyp PCUICContexts PCUICSubstitution
     PCUICWeakeningEnv PCUICWeakeningEnvTyp PCUICEquality
     PCUICWeakeningConv PCUICWeakeningTyp PCUICCumulativity
     PCUICUnivSubst PCUICUnivSubstitutionTyp PCUICGlobalEnv PCUICTyping PCUICGeneration
     PCUICConversion PCUICOnFreeVars
     PCUICValidity PCUICArities PCUICInversion
     PCUICCases PCUICWellScopedCumulativity PCUICSpine PCUICSR
     PCUICSafeLemmata PCUICInductives PCUICInductiveInversion.
From MetaCoq.PCUIC Require Import PCUICExpandLets.
Set Warnings "+notation_overridden".

Import MCMonadNotation.

Implicit Types (cf : checker_flags) (Σ : global_env_ext).
Set Default Proof Using "Type*".

Translation which expands the lets in constructor arguments contexts and the correspomding branches of pattern-matchings, so that let-expansion becomes unnecessary on the resulting terms.

The proof of correctness is complicated by the fact that the translation is valid only on well-scoped terms, at the lowest level, so we carry around `on_free_vars` hypotheses everywhere. Reduction is only preserved when we are translating well-typed terms, as it relies on even stronger invariants on the representation of cases. Finally, the let-expansion of constructor's argument contexts is shown to preserve positivity and the cumulativity relation for cumulative inductive types, which is not entirely trivial.

Source = PCUIC, Target = Coq

Module S := PCUICAst.
Module SE := PCUICEnvironment.
Module ST := PCUICTyping.
Module T := S.
Module TT := ST.

Module SL := PCUICLiftSubst.
Module TL := SL.

Ltac solve_list :=
  rewrite !map_map_compose ?compose_on_snd ?compose_map_def;
  try rewrite !map_length;
  try solve_all; try typeclasses eauto with core.

Lemma mapOne {X Y} (f:X →Y) x:
  map f [x ] = [f x ].
Proof.
  reflexivity.
Qed.

Lemma trans_local_app Γ Δ : trans_local (SE.app_context Γ Δ) = trans_local Γ ,,, trans_local Δ.
Proof.
  now rewrite /trans_local map_app.
Qed.

Lemma forget_types_map_context {term term'} (f : term' → term) ctx :
  forget_types (map_context f ctx) = forget_types ctx.
Proof.
  now rewrite /forget_types map_map_context.
Qed.

Lemma All_fold_map_context (P : context → context_decl → Type) (f : term → term) ctx :
  All_fold P (map_context f ctx) <~> All_fold (fun Γ d ⇒ P (map_context f Γ) (map_decl f d)) ctx.
Proof.
  induction ctx.
  - split; constructor.
  - cbn. split; intros H; depelim H; constructor; auto; now apply IHctx.
Qed.

Lemma on_decl_trans_on_free_vars_decl (Γ : context) n (d : context_decl) :
  ondecl
    (λ t : term ,
     on_free_vars (closedP (#|Γ | + n) xpredT) (trans t)) d →
  on_free_vars_decl
    (shiftnP #|map_context trans Γ | (closedP n xpredT)) (trans_decl d).
Proof.
  intros []. unfold on_free_vars_decl, test_decl.
  destruct d as [na [b|] ty]; cbn in × ⇒ //;
     rewrite map_context_length shiftnP_closedP shiftnP_xpredT //.
  apply/andP. split; auto.
Qed.

Lemma All_fold_closed_on_free_vars_ctx n ctx :
  All_fold (λ Γ : context , ondecl (λ t : term ,
        on_free_vars (closedP (#|Γ | + n) xpredT)
      (trans t))) ctx →
  on_free_vars_ctx (closedP n xpredT) (map_context trans ctx).
Proof.
  intros af.
  eapply on_free_vars_ctx_All_fold.
  eapply All_fold_map_context, All_fold_impl; tea ⇒ ctx' d; cbn.
  now intros; eapply on_decl_trans_on_free_vars_decl.
Qed.

Definition plengths :=
    (@context_assumptions_subst_context ,
    @context_assumptions_app ,
    @context_assumptions_subst_instance , @context_assumptions_lift_context ,
     @expand_lets_ctx_length , @subst_context_length ,
    @subst_instance_length , @expand_lets_k_ctx_length , @inds_length , @lift_context_length ,
    @app_length , @List.rev_length , @extended_subst_length , @reln_length ,
    Nat.add_0_r , @app_nil_r ,
    @map_length , @mapi_length , @mapi_rec_length ,
    @fold_context_k_length , @cofix_subst_length , @fix_subst_length ,
    @smash_context_length , @arities_context_length , @context_assumptions_map ).

Lemma is_assumption_context_spec Γ :
  reflect (PCUICLiftSubst.assumption_context Γ) (is_assumption_context Γ).
Proof.
induction Γ; cbn.
- econstructor. constructor.
- destruct a as [na [b|] ty]; cbn.
   + constructor. intros ass; depelim ass.
   + elim: IHΓ; constructor; pcuic. now constructor.
     apply n; now depelim H.
Qed.

Lemma assumption_context_assumptions Γ :
  assumption_context Γ →
  context_assumptions Γ = #|Γ |.
Proof.
  induction 1; cbn; auto. congruence.
Qed.

Lemma bcontext_trans_length p br : #|bcontext (trans_branch p br)| = context_assumptions (bcontext br).
Proof.
  rewrite /trans_branch.
  elim: is_assumption_context_spec ⇒ ass.
  rewrite assumption_context_assumptions //.
  cbn. rewrite smash_context_length //.
Qed.

Lemma trans_on_free_vars P t :
  on_free_vars P t → on_free_vars P (trans t).
Proof.
  revert P t. eapply term_on_free_vars_ind; cbn; auto;
    lazymatch goal with |- context [case_info] ⇒ idtac | _ ⇒ solve_all end.
  - intros; rtoProp; intuition auto.
    × solve_all.
    × now rewrite map_context_length.
    × rewrite map_length.
      rewrite test_context_k_closed_on_free_vars_ctx.
      now eapply All_fold_closed_on_free_vars_ctx.
    × eapply All_forallb, All_map, All_map, All_impl; tea; cbv beta.
      intros br [hctx ihctx hb ihb]. len.
      rewrite test_context_k_closed_on_free_vars_ctx.
      rewrite /trans_branch.
      elim: is_assumption_context_spec ⇒ isass.
      { cbn [map_branch bcontext]. apply/andP; split.
        now eapply All_fold_closed_on_free_vars_ctx.
        cbn. len. }
      cbn -[on_free_vars_ctx].
      rewrite on_free_vars_ctx_smash //.
      now eapply All_fold_closed_on_free_vars_ctx.
      rewrite /=.
      eapply on_free_vars_expand_lets_k. now len.
      eapply on_free_vars_ctx_subst_context0.
      rewrite !plengths.
      eapply All_fold_closed_on_free_vars_ctx in ihctx.
      rewrite → closedP_shiftnP in ihctx.
      rewrite /id. rewrite on_free_vars_ctx_subst_instance.
      eapply on_free_vars_ctx_impl; tea.
      { unfold shiftnP. intros i. rewrite orb_false_r.
        move/Nat.ltb_lt ⇒ hlt. now apply/orP; left; eapply Nat.ltb_lt. }
      solve_all.
      rewrite !plengths. now apply ihb.
  - unfold test_def. solve_all. cbn. now len in b1.
  - unfold test_def. solve_all. cbn. now len in b1.
Qed.

Lemma on_free_vars_ctx_trans k ctx :
  on_free_vars_ctx (closedP k xpredT) ctx →
  on_free_vars_ctx (closedP k xpredT) (map_context trans ctx).
Proof.
  intros H; apply on_free_vars_ctx_All_fold in H.
  eapply All_fold_closed_on_free_vars_ctx.
  eapply All_fold_impl; tea; cbn.
  intros ? ? h.
  destruct x as [na [b|] ty]; cbn in *;
  constructor; cbn; (move/andP: h ⇒ /= // || move: h) ;
  rewrite ?shiftnP_closedP ?shiftnP_xpredT //;
  intros; try now eapply trans_on_free_vars.
Qed.

Lemma trans_on_free_vars_ctx k ctx :
  on_free_vars_ctx (shiftnP k xpred0) ctx →
  on_free_vars_ctx (shiftnP k xpred0) (map_context trans ctx).
Proof.
  intros hctx.
  rewrite -closedP_shiftnP. eapply on_free_vars_ctx_trans.
  rewrite closedP_shiftnP //.
Qed.

Lemma closedP_mon n n' P i : n ≤ n' → closedP n P i → closedP n' P i.
Proof.
  intros hn; rewrite /closedP.
  repeat nat_compare_specs ⇒ //.
Qed.

Ltac len := rewrite !plengths.

Lemma trans_lift (t : S.term) P n k :
  on_free_vars P t →
  trans (S.lift n k t) = T.lift n k (trans t).
Proof.
  intros onfvs.
  revert P t onfvs k.
  apply: term_on_free_vars_ind; simpl; intros; try congruence.
  - f_equal. rewrite !map_map_compose. solve_all.
  - f_equal; auto.
    rewrite /T.map_predicate_k /id /PCUICAst.map_predicate /= /=.
    f_equal. autorewrite with map; solve_all.
    rewrite map_context_length. solve_all.
    rewrite !map_map_compose.
    eapply All_map_eq, All_impl; tea; cbv beta ⇒ [br [hbctx ihbctx hb ihb]].
    rewrite /trans_branch /T.map_branch_k.
    elim: is_assumption_context_spec ⇒ isass.
    { cbn. rewrite /map_branch /=. f_equal. len. eapply ihb. }
    cbn -[expand_lets].
    len. rewrite (Nat.add_comm (context_assumptions _) k).
    f_equal. rewrite ihb.
    relativize (context_assumptions _).
    erewrite <- expand_lets_lift. 2:len. 2:reflexivity.
    rewrite !plengths.
    rewrite /id. f_equal.
    rewrite distr_lift_subst_context.
    rewrite !plengths. f_equal.
    rewrite map_rev. f_equal. solve_all.
    rewrite PCUICClosed.closed_ctx_lift //.
    rewrite closedn_ctx_on_free_vars.
    rewrite on_free_vars_ctx_subst_instance.
    eapply on_free_vars_ctx_trans. eapply on_free_vars_ctx_impl; tea.
    intros i. eapply closedP_mon. lia.
  - f_equal. solve_all.
  - f_equal; red in X, X0; solve_all.
Qed.

Definition on_fst {A B C} (f:A →C) (p:A ×B) := (f p .1 , p .2 ).

Definition trans_def (decl:def PCUICAst.term) : def term.
Proof.
  destruct decl.
  constructor.
  - exact dname.
  - exact (trans dtype).
  - exact (trans dbody).
  - exact rarg.
Defined.

Lemma trans_global_ext_levels Σ:
  S.global_ext_levels Σ = T.global_ext_levels (trans_global Σ).
Proof. reflexivity. Qed.

Lemma trans_global_ext_constraints Σ :
  S.global_ext_constraints Σ = T.global_ext_constraints (trans_global Σ).
Proof. reflexivity. Qed.

Lemma trans_mem_level_set l Σ:
  LevelSet.mem l (S.global_ext_levels Σ) →
  LevelSet.mem l (T.global_ext_levels (trans_global Σ)).
Proof. auto. Qed.

Lemma trans_in_level_set l Σ :
  LevelSet.In l (S.global_ext_levels Σ) →
  LevelSet.In l (T.global_ext_levels (trans_global Σ)).
Proof. auto. Qed.

Lemma trans_lookup (Σ : global_env) cst :
  lookup_env (trans_global_env Σ) cst = option_map trans_global_decl (SE.lookup_env Σ cst).
Proof.
  cbn in ×.
  destruct Σ as [univs Σ].
  induction Σ.
  - reflexivity.
  - cbn. case: eqb_spec; intros e; subst.
    + destruct a; auto.
    + now rewrite IHΣ.
Qed.

Lemma trans_declared_constant (Σ : global_env) cst decl:
  S.declared_constant Σ cst decl →
  T.declared_constant (trans_global_env Σ) cst (trans_constant_body decl).
Proof.
  unfold T.declared_constant.
  rewrite trans_lookup.
  unfold S.declared_constant.
  intros →.
  reflexivity.
Qed.

Lemma trans_constraintSet_in x Σ:
  ConstraintSet.In x (S.global_ext_constraints Σ) →
  ConstraintSet.In x (T.global_ext_constraints (trans_global Σ)).
Proof.
  rewrite trans_global_ext_constraints.
  trivial.
Qed.

Lemma trans_consistent_instance_ext {cf} Σ decl u:
  S.consistent_instance_ext Σ decl u →
  T.consistent_instance_ext (trans_global Σ) decl u.
Proof. auto. Qed.

Lemma trans_declared_inductive Σ ind mdecl idecl:
  S.declared_inductive Σ ind mdecl idecl →
  T.declared_inductive (trans_global_env Σ) ind (trans_minductive_body mdecl)
   (trans_one_ind_body mdecl (inductive_ind ind) idecl).
Proof.
  intros [].
  split.
  - unfold T.declared_minductive, S.declared_minductive in ×.
    now rewrite trans_lookup H.
  - cbn. now rewrite nth_error_mapi H0 /=.
Qed.

Lemma trans_declared_constructor Σ c mdecl idecl cdecl :
  let ind := (inductive_ind (fst c)) in
  S.declared_constructor Σ c mdecl idecl cdecl →
  T.declared_constructor (trans_global_env Σ) c (trans_minductive_body mdecl) (trans_one_ind_body mdecl ind idecl)
    (trans_constructor_body ind mdecl cdecl).
Proof.
  intros ind [].
  split.
  - now apply trans_declared_inductive.
  - now apply map_nth_error.
Qed.

Lemma trans_mkApps t args:
  trans (PCUICAst.mkApps t args) =
  mkApps (trans t) (map trans args).
Proof.
  induction args in t |- ×.
  - reflexivity.
  - cbn [map].
    cbn.
    rewrite IHargs.
    reflexivity.
Qed.

Lemma trans_decl_type decl:
  trans (decl_type decl) =
  decl_type (trans_decl decl).
Proof.
  destruct decl.
  reflexivity.
Qed.

Lemma expand_lets_subst_comm Γ k s :
  expand_lets (subst_context s k Γ) ∘ subst s (#|Γ | + k) =1
  subst s (context_assumptions Γ + k) ∘ expand_lets Γ.
Proof.
  unfold expand_lets, expand_lets_k; simpl; intros x. len.
  rewrite !PCUICSigmaCalculus.subst_extended_subst.
  rewrite distr_subst. rewrite Nat.add_comm; f_equal; len.
  now rewrite commut_lift_subst_rec.
Qed.

Lemma subst_context_subst_context s k s' Γ :
  subst_context s k (subst_context s' 0 Γ) =
  subst_context (map (subst s k) s') 0 (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 distr_subst_rec; lia_f_equal.
Qed.

Lemma trans_subst p q xs k t :
  on_free_vars p t →
  forallb (on_free_vars q) xs →
  trans (S.subst xs k t) =
  T.subst (map trans xs) k (trans t).
Proof.
  intros onfvs; revert p t onfvs k.
  apply: term_on_free_vars_ind; intros; cbn.
  all: cbn;try congruence.
  - destruct Nat.leb;trivial.
    rewrite nth_error_map.
    destruct nth_error eqn:hnth;cbn.
    2:now rewrite map_length.
    rewrite (trans_lift _ q) //.
    eapply nth_error_forallb in H0; tea.
  - f_equal.
    do 2 rewrite map_map.
    apply All_map_eq.
    solve_all. rewrite b //. solve_all.
  - rewrite H0 // H2 //.
  - rewrite H0 // H2 //.
  - rewrite H0 // H2 // H4 //.
  - rewrite H0 // H2 //.
  - f_equal; trivial.
    rewrite /= /id /T.map_predicate_k /map_predicate_k /map_predicate /=.
    f_equal; solve_all.
    × rewrite b //. solve_all.
    × rewrite H1 //. solve_all. now rewrite map_context_length.
    × rewrite H3 //.
    × rewrite /trans_branch; rewrite !map_map_compose.
      eapply All_map_eq, All_impl; tea; cbv beta; intros.
      destruct X3 as [hctx ihctx hb ihb].
      rewrite /T.map_branch_k /=.
      elim: is_assumption_context_spec ⇒ isass.
      { rewrite /map_branch /= ihb //. f_equal.
        now len. }
      f_equal; auto.
      len ⇒ /=.
      rewrite ihb // /id.
      replace (context_assumptions (map_context trans (bcontext x))) with
        (context_assumptions ((subst_context (List.rev (map trans (pparams pred))) 0
        (map_context trans (bcontext x))@[puinst pred]))). 2:now len.
      cbn.
      relativize (context_assumptions (bcontext x)).
      erewrite <- expand_lets_subst_comm. f_equal. 2:now len.
      2:now len.
      rewrite subst_context_subst_context. f_equal.
      rewrite map_rev; f_equal. solve_all. rewrite b //. solve_all. len.
      rewrite PCUICSpine.closed_ctx_subst //.
      eapply on_free_vars_ctx_trans in hctx.
      rewrite closedn_ctx_on_free_vars.
      rewrite on_free_vars_ctx_subst_instance.
      eapply on_free_vars_ctx_impl; tea.
      intros. eapply closedP_mon; tea. lia.
  - f_equal. rewrite H0 //.
  - f_equal. rewrite !map_map_compose. red in X, X0.
    repeat toAll. eapply All_map_eq, All_impl; tea.
    cbn. rtoProp; intuition auto.
    unfold map_def; cbn. f_equal. rewrite a //. solve_all.
    rewrite b1 //. solve_all. cbn. now len.
  - f_equal. rewrite !map_map_compose.
    repeat toAll. eapply All_map_eq, All_impl; tea.
    cbn. rtoProp; intuition auto.
    unfold map_def; cbn. f_equal. rewrite a //. solve_all.
    rewrite b //. solve_all. now len.
Qed.

Lemma trans_subst_ctx (Γ : context) xs k t :
  on_free_vars (shiftnP (#|xs | + #|Γ |) xpred0) t →
  forallb (on_free_vars (shiftnP #|Γ | xpred0)) xs →
  trans (S.subst xs k t) =
  T.subst (map trans xs) k (trans t).
Proof.
  intros ont onxs.
  now erewrite trans_subst; tea.
Qed.

Lemma trans_subst10 u p q B :
  on_free_vars p B →
  on_free_vars q u →
  trans (S.subst1 u 0 B) =
  T.subst10 (trans u) (trans B).
Proof.
  unfold S.subst1. intros onB onu.
  rewrite (trans_subst p q) //. cbn. now rewrite onu.
Qed.

Lemma trans_subst_instance u t:
  trans (subst_instance u t) =
  subst_instance u (trans t).
Proof.
  induction t in u |- × using PCUICInduction.term_forall_list_ind;cbn;auto;try congruence.
  - do 2 rewrite map_map.
    f_equal.
    apply All_map_eq. solve_all.
  - red in X, X0.
    f_equal.
    + rewrite /map_predicate /=. f_equal. solve_all. solve_all.
    + solve_all.
    + rewrite !map_map_compose. eapply All_map_eq, All_impl; tea; cbv beta.
      intros ? []. rewrite /trans_branch /= /map_branch /= /id.
      elim: is_assumption_context_spec ⇒ isass.
      { f_equal. cbn. now rewrite e. }
      f_equal.
      rewrite PCUICUnivSubstitutionConv.subst_instance_expand_lets e.
      rewrite PCUICUnivSubstitutionConv.subst_instance_subst_context. f_equal.
      f_equal. rewrite [_@[u]]map_rev. f_equal. solve_all.
      solve_all. rewrite [_@[u]] map_map_compose.
      setoid_rewrite compose_map_decl.
      setoid_rewrite PCUICUnivSubstitutionConv.subst_instance_two.
      clear -a. rewrite [_@[_]]map_map_compose.
      rewrite map_map_compose. solve_all.
  - f_equal.
    unfold tFixProp in X. rewrite !map_map_compose. solve_all.
  - f_equal.
    unfold tFixProp in X.
    rewrite !map_map_compose. autorewrite with map. solve_all_one.
Qed.

Lemma trans_subst_instance_ctx Γ u :
  trans_local Γ@[u ] = (trans_local Γ )@[u ].
Proof.
  rewrite /subst_instance /= /trans_local /SE.subst_instance_context /subst_instance_context
    /map_context.
  rewrite !map_map_compose. apply map_ext.
  move ⇒ [na [b|] ty]; cbn;
  rewrite /trans_decl /map_decl /=; f_equal; cbn;
  now rewrite trans_subst_instance.
Qed.

Lemma trans_cst_type decl:
  trans (SE.cst_type decl) =
  cst_type (trans_constant_body decl).
Proof.
  reflexivity.
Qed.

Lemma trans_ind_type mdecl i idecl:
  trans (SE.ind_type idecl) =
  ind_type (trans_one_ind_body mdecl i idecl).
Proof.
  reflexivity.
Qed.

Lemma trans_dtype decl:
  trans (dtype decl) =
  dtype (trans_def decl).
Proof.
  destruct decl.
  reflexivity.
Qed.

Lemma trans_dbody decl:
  trans (dbody decl) =
  dbody (trans_def decl).
Proof.
  destruct decl.
  reflexivity.
Qed.

Lemma trans_inds ind u mdecl :
  map trans (PCUICAst.inds (inductive_mind ind) u (SE.ind_bodies mdecl)) =
  inds (inductive_mind ind) u (ind_bodies (trans_minductive_body mdecl)).
Proof.
  rewrite PCUICCases.inds_spec inds_spec.
  rewrite map_rev map_mapi. simpl.
  f_equal. rewrite mapi_mapi. apply mapi_ext ⇒ n //.
Qed.

Lemma trans_declared_projection Σ p mdecl idecl cdecl pdecl :
  let ind := (inductive_ind p.(proj_ind)) in
  S.declared_projection Σ .1 p mdecl idecl cdecl pdecl →
  T.declared_projection (trans_global Σ ).1 p (trans_minductive_body mdecl) (trans_one_ind_body mdecl ind idecl)
    (trans_constructor_body ind mdecl cdecl) (trans_projection_body pdecl).
Proof.
  intros ind []. split; [|split].
  - now apply trans_declared_constructor.
  - unfold on_snd.
    destruct H0.
    destruct pdecl, p.
    cbn in ×.
    now apply map_nth_error.
  - now destruct mdecl;cbn in ×.
Qed.

Lemma inv_opt_monad {X Y Z} (f:option X) (g:X →option Y) (h:X →Y →option Z) c:
  (x <- f ;;
  y <- g x ;;
  h x y ) = Some c →
  ∃ a b , f = Some a ∧
  g a = Some b ∧ h a b = Some c.
Proof.
  intros H.
  destruct f eqn: ?;cbn in *;try congruence.
  destruct (g x) eqn: ?;cbn in *;try congruence.
  do 2 eexists.
  repeat split;eassumption.
Qed.

Lemma trans_destr_arity x:
  destArity [] (trans x) =
  option_map (fun '(xs ,u ) ⇒ (map trans_decl xs ,u )) (destArity [] x).
Proof.
  set xs := (@nil context_decl). unfold xs at 1.
  replace (@nil context_decl) with (map trans_decl xs) at 1 by (now subst). clearbody xs.
  induction x in xs |- *;cbn;trivial;unfold snoc.
  - rewrite <- IHx2.
    reflexivity.
  - rewrite <- IHx3.
    reflexivity.
Qed.

Lemma trans_mkProd_or_LetIn a t:
  trans (SE.mkProd_or_LetIn a t) =
  mkProd_or_LetIn (trans_decl a) (trans t).
Proof.
  destruct a as [? [] ?];cbn;trivial.
Qed.

Lemma trans_it_mkProd_or_LetIn xs t:
  trans (SE.it_mkProd_or_LetIn xs t) =
  it_mkProd_or_LetIn (map trans_decl xs) (trans t).
Proof.
  induction xs in t |- *;simpl;trivial.
  rewrite IHxs.
  f_equal.
  apply trans_mkProd_or_LetIn.
Qed.

Lemma trans_nth n l x : trans (nth n l x) = nth n (List.map trans l) (trans x).
Proof.
  induction l in n |- *; destruct n; trivial.
  simpl in ×. congruence.
Qed.

Lemma trans_isLambda t :
  T.isLambda (trans t) = S.isLambda t.
Proof.
  destruct t; cbnr.
Qed.

Lemma trans_unfold_fix p mfix idx narg fn :
  on_free_vars p (tFix mfix idx) →
  unfold_fix mfix idx = Some (narg , fn ) →
  unfold_fix (map (map_def trans trans) mfix) idx = Some (narg , trans fn ).
Proof.
  unfold unfold_fix.
  rewrite nth_error_map. destruct (nth_error mfix idx) eqn:Hdef ⇒ //.
  cbn.
  intros onfvs [= <- <-]. simpl.
  repeat f_equal.
  rewrite (trans_subst (shiftnP #|mfix| p) p).
  unshelve eapply nth_error_forallb in onfvs; tea. now move/andP: onfvs ⇒ //.
  eapply (on_free_vars_fix_subst _ _ idx). tea.
  f_equal. clear Hdef. simpl.
  unfold fix_subst. rewrite map_length.
  revert onfvs.
  generalize mfix at 1 2 3 5.
  induction mfix; trivial.
  simpl; intros mfix' hfvs. f_equal.
  now eapply IHmfix.
Qed.

Lemma trans_unfold_cofix p mfix idx narg fn :
  on_free_vars p (tCoFix mfix idx) →
  unfold_cofix mfix idx = Some (narg , fn ) →
  unfold_cofix (map (map_def trans trans) mfix) idx = Some (narg , trans fn ).
Proof.
  unfold unfold_cofix.
  rewrite nth_error_map. destruct (nth_error mfix idx) eqn:Hdef ⇒ //.
  cbn.
  intros onfvs [= <- <-]. simpl.
  repeat f_equal.
  rewrite (trans_subst (shiftnP #|mfix| p) p).
  unshelve eapply nth_error_forallb in onfvs; tea. now move/andP: onfvs ⇒ //.
  eapply (on_free_vars_cofix_subst _ _ idx). tea.
  f_equal. clear Hdef. simpl.
  unfold cofix_subst. rewrite map_length.
  revert onfvs.
  generalize mfix at 1 2 3 5.
  induction mfix; trivial.
  simpl; intros mfix' hfvs. f_equal.
  now eapply IHmfix.
Qed.

Lemma trans_is_constructor:
  ∀ (args : list S.term) (narg : nat),
    is_constructor narg args = true → is_constructor narg (map trans args) = true.
Proof.
  intros args narg.
  unfold is_constructor.
  rewrite nth_error_map //. destruct nth_error ⇒ //. simpl. intros.
  unfold isConstruct_app, decompose_app in ×.
  destruct (decompose_app_rec t []) eqn:da. simpl in H.
  destruct t0 ⇒ //.
  apply decompose_app_rec_inv in da. simpl in da. subst t.
  rewrite trans_mkApps /=.
  rewrite decompose_app_rec_mkApps //.
Qed.

Lemma refine_red1_r Σ Γ t u u' : u = u' → red1 Σ Γ t u → red1 Σ Γ t u'.
Proof.
  intros →. trivial.
Qed.

Lemma refine_red1_Γ Σ Γ Γ' t u : Γ = Γ' → red1 Σ Γ t u → red1 Σ Γ' t u.
Proof.
  intros →. trivial.
Qed.

Lemma forallb_mapi_ext {A B} (p : A → bool) (l : list A) {f g : nat → A → B} :
  forallb p l →
  (∀ i x, p x → f i x = g i x ) →
  mapi f l = mapi g l.
Proof.
  unfold mapi; generalize 0. induction l; cbn; auto.
  move⇒ n /andP[] pa pl hf.
  rewrite hf //. f_equal. apply IHl ⇒ //.
Qed.

Lemma trans_fix_context p mfix idx :
  on_free_vars p (tFix mfix idx) →
  map trans_decl (SE.fix_context mfix) =
  fix_context (map (map_def trans trans) mfix).
Proof.
  unfold trans_local.
  unfold fix_context.
  rewrite map_rev map_mapi.
  cbn. move⇒ onfvs. f_equal.
  rewrite mapi_map. eapply forallb_mapi_ext; tea ⇒ i x hx.
  cbn. rewrite /trans_decl /= /vass. f_equal.
  rewrite (trans_lift _ p) //.
  now move/andP: hx.
Qed.

Lemma trans_subst_decl p q s k d :
  on_free_vars_terms p s →
  on_free_vars_decl q d →
  trans_decl (SE.subst_decl s k d) = subst_decl (map trans s) k (trans_decl d).
Proof.
  destruct d as [na [b|] ty]; cbn; rewrite /trans_decl /= /subst_decl /= /map_decl /=.
  intros ons ond.
  f_equal. f_equal.
  rewrite (trans_subst q p) //.
  now move/andP: ond ⇒ /=.
  rewrite (trans_subst q p) //.
  now move/andP: ond ⇒ /=.
  intros ons ond.
  f_equal. f_equal.
  rewrite (trans_subst q p) //.
Qed.

Lemma trans_subst_context p q s k Γ :
  on_free_vars_ctx p Γ →
  on_free_vars_terms q s →
  trans_local (SE.subst_context s k Γ) = subst_context (map trans s) k (trans_local Γ).
Proof.
  induction Γ as [|d Γ]; simpl; auto.
  rewrite !subst_context_snoc /= on_free_vars_ctx_snoc.
  move⇒ /andP[] onΓ ond ons.
  erewrite trans_subst_decl; tea. rewrite /app_context /snoc. len. f_equal.
  now apply IHΓ.
Qed.

Lemma trans_lift_decl p n k d :
  on_free_vars_decl p d →
  trans_decl (SE.lift_decl n k d) = lift_decl n k (trans_decl d).
Proof.
  destruct d as [na [b|] ty]; cbn; rewrite /trans_decl /= /lift_decl /= /map_decl /=.
  intros ond.
  f_equal. f_equal.
  rewrite (trans_lift _ p) //.
  now move/andP: ond ⇒ /=.
  rewrite (trans_lift _ p) //.
  now move/andP: ond ⇒ /=.
  intros ond.
  f_equal. f_equal.
  rewrite (trans_lift _ p) //.
Qed.

Lemma trans_lift_context p n k Γ :
  on_free_vars_ctx p Γ →
  trans_local (SE.lift_context n k Γ) = lift_context n k (trans_local Γ).
Proof.
  induction Γ as [|d]; auto.
  rewrite /= !lift_context_snoc /= on_free_vars_ctx_snoc.
  move/andP ⇒ [] onΓ ond.
  rewrite (trans_lift_decl (shiftnP #|Γ| p)) //. len. unfold snoc. f_equal.
  now apply IHΓ.
Qed.

Lemma trans_smash_context p Γ Δ :
  on_free_vars_ctx (shiftnP #|Δ | p) Γ →
  on_free_vars_ctx p Δ →
  trans_local (SE.smash_context Γ Δ) = smash_context (trans_local Γ) (trans_local Δ).
Proof.
  induction Δ in p, Γ |- *; simpl; auto.
  rewrite on_free_vars_ctx_snoc.
  move⇒ onΓ /andP [] onΔ ona.
  destruct a as [na [b|] ty] ⇒ /=.
  rewrite (IHΔ p) //.
  eapply on_free_vars_ctx_subst_context0.
  now rewrite shiftnP_add. cbn.
  move/andP: ona ⇒ [] /= → //.
  f_equal.
  rewrite (trans_subst_context (shiftnP (S #|Δ|) p) (shiftnP #|Δ| p)) //.
  move/andP: ona ⇒ [] /= → //; cbn; auto.
  rewrite (IHΔ p) //.
  rewrite on_free_vars_ctx_app /=.
  cbn. rewrite shiftnP0. move/andP: ona ⇒ [] _ →.
  now rewrite shiftnP_add. f_equal. rewrite trans_local_app //.
Qed.

Lemma context_assumptions_map ctx : context_assumptions (map trans_decl ctx) = SE.context_assumptions ctx.
Proof.
  induction ctx as [|[na [b|] ty] ctx]; simpl; auto; lia.
Qed.

Lemma on_free_vars_ctx_k_eq p n Γ :
  on_free_vars_ctx_k p n Γ = on_free_vars_ctx (shiftnP n p) Γ.
Proof.
  rewrite /on_free_vars_ctx_k.
  rewrite alli_shift //.
  rewrite /on_free_vars_ctx.
  eapply alli_ext. intros i x.
  now rewrite shiftnP_add Nat.add_comm.
Qed.

Lemma trans_extended_subst p Γ n :
  on_free_vars_ctx p Γ →
  map trans (extended_subst Γ n) = extended_subst (trans_local Γ) n.
Proof.
  induction Γ in n, p |- *; simpl; auto.
  destruct a as [na [b|] ty]; simpl; auto.
  rewrite on_free_vars_ctx_snoc. move/andP ⇒ [] onΓ /andP[] onb onty.
  erewrite (trans_subst _ _); revgoals.
  eapply on_free_vars_extended_subst.
  erewrite on_free_vars_ctx_k_eq ⇒ //.
  eapply on_free_vars_ctx_impl; tea. intros i pi. rewrite /shiftnP.
  nat_compare_specs; cbn. auto. now instantiate (1 := xpredT).
  erewrite on_free_vars_lift. eapply onb.
  erewrite (trans_lift _ _); revgoals. eapply onb.
  rewrite (IHΓ p) //. f_equal. f_equal. now len.
  rewrite on_free_vars_ctx_snoc ⇒ /andP[] onΓ ont.
  f_equal; eauto.
Qed.

Lemma trans_expand_lets_k p Γ k T :
  on_free_vars_ctx p Γ →
  on_free_vars (shiftnP #|Γ | p) T →
  trans (SE.expand_lets_k Γ k T) = expand_lets_k (trans_local Γ) k (trans T).
Proof.
  rewrite /SE.expand_lets_k ⇒ onΓ onT.
  erewrite (trans_subst _ _); revgoals.
  eapply on_free_vars_extended_subst. rewrite on_free_vars_ctx_k_eq shiftnP0. exact onΓ.
  erewrite on_free_vars_lift. exact onT.
  erewrite (trans_lift _) ⇒ //. 2:exact onT.
  erewrite trans_extended_subst; tea.
  rewrite /expand_lets /expand_lets_k.
  now len.
Qed.

Lemma trans_expand_lets p Γ T :
  on_free_vars_ctx p Γ →
  on_free_vars (shiftnP #|Γ | p) T →
  trans (expand_lets Γ T) = expand_lets (trans_local Γ) (trans T).
Proof.
  move⇒ onΓ onT.
  rewrite /SE.expand_lets /SE.expand_lets_k.
  rewrite (trans_expand_lets_k p) //.
Qed.

Lemma trans_expand_lets_map p Γ T :
  on_free_vars_ctx p Γ →
  on_free_vars_terms (shiftnP #|Γ | p) T →
  map trans (map (expand_lets Γ) T) = map (expand_lets (trans_local Γ)) (map trans T).
Proof.
  move⇒ onΓ onT.
  eapply forallb_All in onT. solve_all.
  rewrite (trans_expand_lets p) //.
Qed.

Lemma alpha_eq_trans {Γ Δ} :
  eq_context_upto_names Γ Δ →
  eq_context_upto_names (trans_local Γ) (trans_local Δ).
Proof.
  intros.
  eapply All2_map, All2_impl; tea.
  intros x y []; constructor; subst; auto.
Qed.

Definition wt {cf} Σ Γ t := ∑ T , Σ ;;; Γ |- t : T.

Lemma isType_wt {cf} {Σ Γ T} : isType Σ Γ T → wt Σ Γ T.
Proof.
  intros [s hs]; now ∃ (PCUICAst.tSort s).
Qed.
Coercion isType_wt : isType >-> wt.

Lemma wt_wf_local {cf} {Σ} {Γ t} : wt Σ Γ t → wf_local Σ Γ.
Proof.
  intros [s hs]. now eapply typing_wf_local.
Qed.

Coercion wt_wf_local : wt >-> All_local_env.

Lemma wt_red {cf} {Σ : global_env_ext} {wfΣ : wf Σ} {Γ t u} : wt Σ Γ t → red1 Σ Γ t u → wt Σ Γ u.
Proof.
  intros [s hs] r. ∃ s.
  eapply subject_reduction; tea. now apply red1_red.
Qed.

Section wtsub.
  Context {cf} {Σ : PCUICEnvironment.global_env_ext} {wfΣ : PCUICTyping.wf Σ}.
  Import PCUICAst.
  Definition wt_subterm Γ (t : term) : Type :=
    let wt := wt Σ in
    match t with
    | tLambda na A B ⇒ wt Γ A × wt (Γ ,, vass na A) B
    | tProd na A B ⇒ wt Γ A × wt (Γ ,, vass na A) B
    | tLetIn na b ty b' ⇒ [× wt Γ b, wt Γ ty & wt (Γ ,, vdef na b ty) b']
    | tApp f a ⇒ wt Γ f × wt Γ a
    | tCase ci p c brs ⇒
      All (wt Γ) p.(pparams) ×
      ∑ mdecl idecl ,
      [× declared_inductive Σ ci mdecl idecl ,
         consistent_instance_ext Σ (PCUICEnvironment.ind_universes mdecl) (PCUICAst.puinst p),
         wf_predicate mdecl idecl p,
         All2 (PCUICEquality.compare_decls eq eq) (PCUICCases.ind_predicate_context ci mdecl idecl) (PCUICAst.pcontext p),
         wf_local_rel Σ (Γ ,,, smash_context [] (ind_params mdecl )@[p.(puinst)]) p.(pcontext)@[p.(puinst)],
         PCUICSpine.spine_subst Σ Γ (PCUICAst.pparams p) (List.rev (PCUICAst.pparams p))
          (PCUICEnvironment.smash_context [] (PCUICEnvironment.ind_params mdecl )@[PCUICAst.puinst p]),
          wt (Γ ,,, PCUICCases.case_predicate_context ci mdecl idecl p) p.(preturn),
          wt Γ c &
          All2i (fun i cdecl br ⇒
            [× wf_branch cdecl br ,
               All2 (PCUICEquality.compare_decls eq eq) (bcontext br) (PCUICCases.cstr_branch_context ci mdecl cdecl),
               wf_local_rel Σ (Γ ,,, smash_context [] (ind_params mdecl )@[p.(puinst)]) br.(bcontext)@[p.(puinst)],
               All2 (PCUICEquality.compare_decls eq eq)
                (Γ ,,, PCUICCases.case_branch_context ci mdecl p (forget_types br.(bcontext)) cdecl)
                (Γ ,,, inst_case_branch_context p br) &
              wt (Γ ,,, PCUICCases.case_branch_context ci mdecl p (forget_types br.(bcontext)) cdecl) br.(bbody)]) 0 idecl.(ind_ctors) brs]
    | tProj p c ⇒ wt Γ c
    | tFix mfix idx | tCoFix mfix idx ⇒
      All (fun d ⇒ wt Γ d.(dtype) × wt (Γ ,,, fix_context mfix) d.(dbody)) mfix
    | tEvar _ l ⇒ False
    | tRel i ⇒ wf_local Σ Γ
    | _ ⇒ unit
    end.
  Import PCUICGeneration PCUICInversion.

  Lemma spine_subst_wt Γ args inst Δ : PCUICSpine.spine_subst Σ Γ args inst Δ →
    All (wt Σ Γ) inst.
  Proof.
    intros []. clear -inst_subslet wfΣ.
    induction inst_subslet; constructor; auto.
    eexists; tea. eexists; tea.
  Qed.

  Lemma wt_inv {Γ t} : wt Σ Γ t → wt_subterm Γ t.
  Proof.
    destruct t; simpl; intros [T h]; try exact tt.
    - now eapply typing_wf_local in h.
    - now eapply inversion_Evar in h.
    - eapply inversion_Prod in h as (?&?&?&?&?); tea.
      split; eexists; eauto.
    - eapply inversion_Lambda in h as (?&?&?&?&?); tea.
      split; eexists; eauto.
    - eapply inversion_LetIn in h as (?&?&?&?&?&?); tea.
      repeat split; eexists; eauto.
    - eapply inversion_App in h as (?&?&?&?&?&?); tea.
      split; eexists; eauto.
    - eapply inversion_Case in h as (mdecl&idecl&decli&indices&[]&?); tea.
      assert (tty := PCUICValidity.validity scrut_ty).
      eapply PCUICInductiveInversion.isType_mkApps_Ind_smash in tty as []; tea.
      2:eapply (wf_predicate_length_pars wf_pred).
      split.
      eapply spine_subst_wt in s. now eapply All_rev_inv in s.
      ∃ mdecl, idecl. split; auto. now symmetry.
      × eapply wf_local_app_inv. eapply wf_local_alpha.
        eapply All2_app; [|reflexivity].
        eapply alpha_eq_subst_instance. symmetry; tea.
        eapply wf_ind_predicate; tea. pcuic.
      × eexists; tea.
      × eexists; tea.
      × eapply Forall2_All2 in wf_brs.
        eapply All2i_All2_mix_left in brs_ty; tea.
        eapply All2i_nth_hyp in brs_ty.
        solve_all. split; auto.
        { eapply wf_local_app_inv. eapply wf_local_alpha.
          eapply All2_app; [|reflexivity].
          eapply alpha_eq_subst_instance in a2.
          symmetry; tea.
          eapply validity in scrut_ty.
          epose proof (wf_case_branch_type ps _ decli scrut_ty wf_pred pret_ty conv_pctx i x y).
          forward X. { split; eauto. }
          specialize (X a1) as [].
          eapply wf_local_expand_lets in a5.
          rewrite /PCUICCases.cstr_branch_context.
          rewrite PCUICUnivSubstitutionConv.subst_instance_expand_lets_ctx.
          rewrite PCUICUnivSubstitutionConv.subst_instance_subst_context.
          rewrite PCUICUnivSubstitutionConv.subst_instance_inds.
          erewrite PCUICUnivSubstitutionConv.subst_instance_id_mdecl; tea. }
        erewrite PCUICCasesContexts.inst_case_branch_context_eq; tea. reflexivity.
        eexists; tea.
    - eapply inversion_Proj in h as (?&?&?&?&?&?&?&?&?); tea.
      eexists; eauto.
    - eapply inversion_Fix in h as (?&?&?&?&?&?&?); tea.
      eapply All_prod.
      eapply (All_impl a). intros ? h; exact h.
      eapply (All_impl a0). intros ? h; eexists; tea.
    - eapply inversion_CoFix in h as (?&?&?&?&?&?&?); tea.
      eapply All_prod.
      eapply (All_impl a). intros ? h; exact h.
      eapply (All_impl a0). intros ? h; eexists; tea.
  Qed.
End wtsub.

Ltac outtimes :=
  match goal with
  | ih : _ × _ |- _ ⇒
    destruct ih as [? ?]
  end.

Lemma red1_cumul {cf} (Σ : global_env_ext) Γ T U : red1 Σ Γ T U → cumulAlgo Σ Γ T U.
Proof.
  intros r.
  econstructor 2; tea. constructor. reflexivity.
Qed.

Lemma red1_cumul_inv {cf} (Σ : global_env_ext) Γ T U : red1 Σ Γ T U → cumulAlgo Σ Γ U T.
Proof.
  intros r.
  econstructor 3; tea. constructor. reflexivity.
Qed.

Definition TTconv {cf} (Σ : global_env_ext) Γ : relation term :=
  clos_refl_sym_trans (relation_disjunction (red1 Σ Γ) (eq_term Σ (T.global_ext_constraints Σ))).

Lemma red1_conv {cf} (Σ : global_env_ext) Γ T U : red1 Σ Γ T U → TTconv Σ Γ T U.
Proof.
  intros r.
  now repeat constructor.
Qed.

Lemma trans_expand_lets_ctx p q Γ Δ :
  on_free_vars_ctx p Γ →
  on_free_vars_ctx q Δ →
  trans_local (SE.expand_lets_ctx Γ Δ) = expand_lets_ctx (trans_local Γ) (trans_local Δ).
Proof.
  move⇒ onΓ onΔ.
  rewrite /SE.expand_lets_ctx /SE.expand_lets_k_ctx /expand_lets_ctx /expand_lets_k_ctx.
  erewrite trans_subst_context.
  erewrite trans_extended_subst; tea.
  erewrite trans_lift_context; tea.
  rewrite context_assumptions_map map_length //.
  erewrite <- on_free_vars_ctx_lift_context; tea.
  eapply on_free_vars_extended_subst. rewrite on_free_vars_ctx_k_eq shiftnP0; tea.
Qed.

Lemma trans_cstr_branch_context p i ci mdecl cdecl :
  on_free_vars_ctx p (ind_params mdecl) →
  on_free_vars_ctx (shiftnP (#|ind_params mdecl | + #|ind_bodies mdecl |) xpred0) (cstr_args cdecl) →
  smash_context [] (trans_local (PCUICCases.cstr_branch_context ci mdecl cdecl)) =
  cstr_branch_context ci (trans_minductive_body mdecl) (trans_constructor_body i mdecl cdecl).
Proof.
  move⇒ onpars onargs.
  rewrite /PCUICCases.cstr_branch_context /cstr_branch_context.
  erewrite trans_expand_lets_ctx; tea.
  erewrite trans_subst_context; tea.
  erewrite trans_inds.
  rewrite -(PCUICContexts.expand_lets_smash_context _ []).
  f_equal.
  rewrite PCUICContexts.smash_context_subst_empty.
  f_equal ⇒ //. now cbn; rewrite map_length.
  eapply (inds_is_open_terms []).
  eapply on_free_vars_ctx_subst_context. len. exact onargs.
  eapply (inds_is_open_terms []).
Qed.

Lemma trans_cstr_branch_context_inst p i ci mdecl cdecl u :
  on_free_vars_ctx p (ind_params mdecl) →
  on_free_vars_ctx (shiftnP (#|ind_params mdecl | + #|ind_bodies mdecl |) xpred0) (cstr_args cdecl) →
  smash_context [] (trans_local (PCUICCases.cstr_branch_context ci mdecl cdecl )@[u ]) =
  (cstr_branch_context ci (trans_minductive_body mdecl) (trans_constructor_body i mdecl cdecl))@[u ].
Proof.
  move⇒ onps onargs.
  rewrite trans_subst_instance_ctx -(PCUICUnivSubstitutionConv.subst_instance_smash _ _ []).
  rewrite (trans_cstr_branch_context p i) //.
Qed.

Require Import PCUICContexts.

Lemma eq_names_smash_context Γ :
  All2 (fun x y ⇒ decl_name x = decl_name y) (smash_context [] (trans_local Γ)) (smash_context [] Γ).
Proof.
  induction Γ.
  × constructor.
  × destruct a as [na [b|] ty]; cbn; auto.
    rewrite smash_context_acc (smash_context_acc _ [_]). constructor; auto.
Qed.

Lemma trans_assumption_context Γ : assumption_context Γ ↔ assumption_context (trans_local Γ).
Proof.
  induction Γ; cbn; auto. reflexivity.
  split.
  - intros ass; depelim ass; constructor; auto.
    now apply IHΓ.
  - intros ass; destruct a as [na [b|] ty]; depelim ass; constructor.
    now apply IHΓ.
Qed.

Lemma trans_inst_case_branch_context_gen p q pred i br ci mdecl cdecl :
  let pred' := PCUICAst.map_predicate id trans trans (map_context trans) pred in
  wf_branch cdecl br →
  on_free_vars_ctx p (ind_params mdecl) →
  on_free_vars_ctx (shiftnP (#|ind_params mdecl | + #|ind_bodies mdecl |) xpred0)
    (cstr_args cdecl) →
  on_free_vars_terms q pred.(pparams) →
  on_free_vars_ctx (shiftnP #|pred.(pparams)| xpred0) br.(bcontext) →

  eq_context_upto_names br.(PCUICAst.bcontext) (PCUICCases.cstr_branch_context ci mdecl cdecl) →
  let br' := trans_branch pred' (map_branch trans (map_context trans) br) in
  (case_branch_context ci
    (trans_minductive_body mdecl) pred' (forget_types br'.(bcontext)) (trans_constructor_body i mdecl cdecl)) =
    (trans_local (smash_context [] (inst_case_branch_context pred br))).
Proof.
  intros p' wfbr onindpars onargs onpars onbctx.
  rewrite /inst_case_branch_context.
  rewrite /inst_case_context.
  rewrite /case_branch_context /case_branch_context_gen.
  rewrite (trans_smash_context q) //.
  { eapply on_free_vars_ctx_impl. 2:eapply on_free_vars_ctx_subst_context.
    3:rewrite forallb_rev //; tea.
    intros i'; rewrite shiftnP0 //.
    len. rewrite on_free_vars_ctx_subst_instance //.
    eapply on_free_vars_ctx_impl; tea.
    intros o. rewrite /shiftnP /=. rewrite orb_false_r.
    repeat nat_compare_specs; auto ⇒ //. }
  rewrite (trans_subst_context (shiftnP #|pred.(pparams)| xpred0) q).
  { rewrite on_free_vars_ctx_subst_instance //. }
  { rewrite [on_free_vars_terms _ _]forallb_rev //. }
  intros eq.
  rewrite map_rev.
  rewrite PCUICContexts.smash_context_subst_empty.
  eapply map2_set_binder_name_alpha_eq.
  { apply eq_names_subst_context.
    eapply All2_map_left.
    rewrite -(trans_smash_context (shiftnP #|pred.(pparams)| xpred0) []) //.
    { rewrite on_free_vars_ctx_subst_instance //. }
    eapply All2_map_right.
    rewrite -(PCUICUnivSubstitutionConv.subst_instance_smash _ _ []).
    eapply All2_map_right; cbn.
    rewrite /trans_branch.
    elim: is_assumption_context_spec ⇒ isass. cbn. cbn in isass.
    { eapply trans_assumption_context in isass.
      rewrite smash_assumption_context //.
      eapply All2_map_left ⇒ /=. apply All2_refl. reflexivity. }
    apply eq_names_smash_context. }
  eapply alpha_eq_subst_context.
  eapply alpha_eq_subst_instance in eq.
  symmetry in eq.
  eapply alpha_eq_trans in eq.
  rewrite -(trans_cstr_branch_context_inst p i) //.
  eapply alpha_eq_smash_context. exact eq.
Qed.

Lemma alpha_eq_on_free_vars_ctx {p Γ Δ} :
  eq_context_upto_names Γ Δ →
  on_free_vars_ctx p Γ →
  on_free_vars_ctx p Δ.
Proof.
  induction 1 ⇒ //.
  rewrite !on_free_vars_ctx_snoc⇒ /andP[] clx cll.
  apply /andP; split; auto.
  destruct r; unfold ws_decl, test_decl in *; cbn in *; subst; auto; now rewrite -(All2_length X).
Qed.

Lemma trans_inst_case_branch_context {cf} {Σ : global_env_ext} {wfΣ : wf Σ}
  {Γ : context} {pred i br ci c mdecl idecl cdecl} :
  let pred' := PCUICAst.map_predicate id trans trans (map_context trans) pred in
  let br' := trans_branch pred' (map_branch trans (map_context trans) br) in
  wf_predicate mdecl idecl pred →
  wf_branch cdecl br →
  declared_constructor Σ (ci , c ) mdecl idecl cdecl →
  on_free_vars_terms (shiftnP #|Γ | xpred0) pred.(pparams) →
  eq_context_upto_names br.(PCUICAst.bcontext) (PCUICCases.cstr_branch_context ci mdecl cdecl) →
  (case_branch_context ci
    (trans_minductive_body mdecl) pred' (forget_types br'.(bcontext)) (trans_constructor_body i mdecl cdecl)) =
    (trans_local (smash_context [] (inst_case_branch_context pred br))).
Proof.
  intros pred' br' wfp wfbr declc onps com.
  eapply (trans_inst_case_branch_context_gen xpred0 (shiftnP #|Γ| xpred0)) ⇒ //.
  eapply closed_ctx_on_free_vars; eapply (declared_inductive_closed_params declc).
  rewrite -closedn_ctx_on_free_vars. rewrite Nat.add_comm; eapply (declared_constructor_closed_args declc).
  eapply alpha_eq_on_free_vars_ctx. symmetry; tea.
  rewrite -closedn_ctx_on_free_vars.
  relativize #|pparams pred|. eapply (closed_cstr_branch_context declc).
  rewrite (wf_predicate_length_pars wfp).
  now rewrite (declared_minductive_ind_npars declc).
Qed.

Require Import PCUICSpine.

Lemma trans_reln l p Γ : map trans (SE.reln l p Γ) =
  reln (map trans l) p (trans_local Γ).
Proof.
  induction Γ as [|[na [b|] ty] Γ] in l, p |- *; simpl; auto.
  now rewrite IHΓ.
Qed.

Lemma trans_to_extended_list Γ n : map trans (SE.to_extended_list_k Γ n) = to_extended_list_k (trans_local Γ) n.
Proof.
  now rewrite /to_extended_list_k trans_reln.
Qed.

Lemma trans_ind_predicate_context ci mdecl idecl :
  is_closed_context (ind_params mdecl) →
  on_free_vars_ctx (shiftnP #|ind_params mdecl | xpred0) (ind_indices idecl) →
  trans_local (PCUICCases.ind_predicate_context ci mdecl idecl) =
  (ind_predicate_context ci (trans_minductive_body mdecl)
      (trans_one_ind_body mdecl (inductive_ind ci) idecl)).
Proof.
  move⇒ clpars clindices.
  rewrite /ind_predicate_context /Ast.ind_predicate_context /=.
  rewrite /trans_decl /=. f_equal.
  f_equal. rewrite trans_mkApps /=. f_equal.
  rewrite trans_to_extended_list trans_local_app /to_extended_list.
  f_equal. f_equal.
  now rewrite (trans_smash_context xpred0).
  now rewrite (trans_expand_lets_ctx xpred0 (shiftnP #|ind_params mdecl| xpred0)).
  now rewrite (trans_expand_lets_ctx xpred0 (shiftnP #|ind_params mdecl| xpred0)).
Qed.

Lemma trans_ind_predicate_context_eq p ci mdecl idecl :
  is_closed_context (ind_params mdecl) →
  on_free_vars_ctx (shiftnP #|ind_params mdecl | xpred0) (ind_indices idecl) →
  eq_context_upto_names (PCUICAst.pcontext p)
    (PCUICCases.ind_predicate_context ci mdecl idecl) →
  All2
    (λ (x : binder_annot name) (y : context_decl ),
       eq_binder_annot x (decl_name y))
    (map decl_name (trans_local (PCUICAst.pcontext p)))
    (ind_predicate_context ci (trans_minductive_body mdecl)
       (trans_one_ind_body mdecl (inductive_ind ci) idecl)).
Proof.
  move⇒ clpars clindices.
  rewrite -trans_ind_predicate_context //.
  intros. eapply All2_map, All2_map_left.
  solve_all.
  destruct X; cbn; subst; auto.
Qed.

Lemma trans_cstr_branch_context_eq ci mdecl cdecl p i br :
  is_closed_context (ind_params mdecl) →
  on_free_vars_ctx (shiftnP (#|ind_params mdecl | + #|ind_bodies mdecl |) xpred0)
  (cstr_args cdecl) →
  eq_context_upto_names (PCUICAst.bcontext br)
    (PCUICCases.cstr_branch_context ci mdecl cdecl) →
  eq_context_upto_names
    (bcontext (trans_branch p (map_branch trans (map_context trans) br)))
    (cstr_branch_context ci (trans_minductive_body mdecl)
      (trans_constructor_body i mdecl cdecl)).
Proof.
  intros clpars clargs a.
  rewrite -(trans_cstr_branch_context xpred0) //.
  cbn.
  rewrite /trans_branch.
  elim: is_assumption_context_spec ⇒ isass.
  { cbn in isass |- ×.
    rewrite -(smash_assumption_context (map_context trans (bcontext br))) //.
    eapply alpha_eq_smash_context.
    eapply All2_map. solve_all.
    destruct X; subst; auto; constructor; cbn; auto. }
  { eapply alpha_eq_smash_context.
    eapply All2_map. solve_all.
    destruct X; subst; auto; constructor; cbn; auto. }
Qed.

Lemma map_map2 {A B C D} (f : A → B) (g : C → D → A) l l' :
  map f (map2 g l l') = map2 (fun x y ⇒ f (g x y)) l l'.
Proof.
  induction l in l' |- *; destruct l'; simpl; auto.
  now rewrite IHl.
Qed.

Lemma map2_map_map {A B C D} (f : A → B → C) (g : D → B) l l' :
  map2 (fun x y ⇒ f x (g y)) l l' = map2 f l (map g l').
Proof.
  induction l in l' |- *; destruct l'; simpl; auto.
  now rewrite IHl.
Qed.

Lemma trans_set_binder na y :
  trans_decl (PCUICEnvironment.set_binder_name na y) = set_binder_name na (trans_decl y).
Proof.
  destruct y as [na' [b|] ty]; cbn; auto.
Qed.

Require Import Morphisms.
#[global] Instance map2_Proper {A B C} : Morphisms.Proper (pointwise_relation A (pointwise_relation B (@eq C)) ==> eq ==> eq ==> eq) map2.
Proof.
  intros f g Hfg ? ? → ? ? →.
  eapply map2_ext, Hfg.
Qed.

Lemma map2_set_binder_name_eq nas Δ Δ' :
  eq_context_upto_names Δ Δ' →
  map2 set_binder_name nas Δ = map2 set_binder_name nas Δ'.
Proof.
  induction 1 in nas |- *; cbn; auto.
  destruct nas; cbn; auto.
  rewrite IHX. destruct r; subst; cbn; reflexivity.
Qed.

Lemma eq_binder_trans (nas : list aname) (Δ : PCUICEnvironment.context) :
  All2 (fun x y ⇒ eq_binder_annot x (decl_name y)) nas Δ →
  All2 (fun x y ⇒ eq_binder_annot x (decl_name y)) nas (trans_local Δ).
Proof.
  intros. eapply All2_map_right, All2_impl; tea.
  cbn. intros x y H. destruct y; apply H.
Qed.

Lemma trans_local_set_binder nas Γ :
  trans_local (map2 PCUICEnvironment.set_binder_name nas Γ) =
  map2 set_binder_name nas (trans_local Γ).
Proof.
  rewrite /trans_local map_map2.
  setoid_rewrite trans_set_binder.
  now rewrite map2_map_map.
Qed.

Lemma All2_eq_binder_lift_context (l : list (binder_annot name)) n k (Γ : PCUICEnvironment.context) :
  All2 (fun x y ⇒ eq_binder_annot x y.(decl_name)) l Γ →
  All2 (fun x y ⇒ eq_binder_annot x y.(decl_name)) l (PCUICEnvironment.lift_context n k Γ).
Proof.
  induction 1; cbn; rewrite ?PCUICLiftSubst.lift_context_snoc //; constructor; auto.
Qed.

Lemma All2_eq_binder_expand_lets_ctx (l : list (binder_annot name)) (Δ Γ : PCUICEnvironment.context) :
  All2 (fun x y ⇒ eq_binder_annot x y.(decl_name)) l Γ →
  All2 (fun x y ⇒ eq_binder_annot x y.(decl_name)) l (PCUICEnvironment.expand_lets_ctx Δ Γ).
Proof.
  intros a.
  now eapply All2_eq_binder_subst_context, All2_eq_binder_lift_context.
Qed.

Lemma trans_local_set_binder_name_eq nas Γ Δ :
  All2 (PCUICEquality.compare_decls eq eq) Γ Δ →
  trans_local (map2 PCUICEnvironment.set_binder_name nas Γ) =
  trans_local (map2 PCUICEnvironment.set_binder_name nas Δ).
Proof.
  induction 1 in nas |- *; cbn; auto.
  destruct nas; cbn; auto.
  f_equal. destruct r; subst; f_equal.
  apply IHX.
Qed.

Lemma map2_trans l l' :
  map2
  (λ (x : aname) (y : PCUICEnvironment.context_decl ),
      trans_decl (PCUICEnvironment.set_binder_name x y)) l l' =
  map2 (fun (x : aname) (y : PCUICEnvironment.context_decl) ⇒
    set_binder_name x (trans_decl y)) l l'.
Proof.
  eapply map2_ext.
  intros x y. rewrite /trans_decl. now destruct y; cbn.
Qed.

Lemma closed_ctx_is_closed_context Γ :
  closed_ctx Γ → is_closed_context Γ.
Proof.
  now rewrite closedn_ctx_on_free_vars closedP_shiftnP shiftnP0.
Qed.
#[local] Hint Resolve closed_ctx_is_closed_context : pcuic.
#[local] Hint Resolve declared_inductive_closed_params : pcuic.

Lemma closedn_ctx_on_free_vars n (Δ : context) :
  closedn_ctx n Δ → on_free_vars_ctx (shiftnP n xpred0) Δ.
Proof.
  rewrite closedn_ctx_on_free_vars closedP_shiftnP //.
Qed.

#[local] Hint Resolve closedn_ctx_on_free_vars : pcuic.

Lemma declared_inductive_closed_indices {cf} {Σ : PCUICEnvironment.global_env_ext}
  {wfΣ : PCUICTyping.wf Σ} ind mdecl idecl :
  declared_inductive Σ ind mdecl idecl →
  closedn_ctx #|ind_params mdecl | (ind_indices idecl).
Proof.
  move/declared_inductive_closed_pars_indices.
  rewrite closedn_ctx_app /= ⇒ /andP[] //.
Qed.
#[local] Hint Resolve declared_inductive_closed_indices : pcuic.

Lemma on_free_vars_ind_predicate_context {cf : checker_flags} {Σ : global_env_ext} {wfΣ : wf Σ} {ind mdecl idecl} :
  declared_inductive Σ ind mdecl idecl →
  on_free_vars_ctx (closedP (context_assumptions (ind_params mdecl)) xpredT)
    (ind_predicate_context ind mdecl idecl).
Proof.
  intros decli.
  rewrite <- PCUICOnFreeVars.closedn_ctx_on_free_vars.
  eapply PCUICClosed.closed_ind_predicate_context; tea.
  eapply (PCUICClosedTyp.declared_minductive_closed (proj1 decli)).
Qed.

Lemma trans_case_predicate_context {cf} {Σ : PCUICEnvironment.global_env_ext}
  {wfΣ : PCUICTyping.wf Σ} {Γ ci mdecl idecl p} :
  S.declared_inductive Σ ci mdecl idecl →
  S.consistent_instance_ext Σ (PCUICEnvironment.ind_universes mdecl) (PCUICAst.puinst p) →
  let parctx := (PCUICEnvironment.ind_params mdecl )@[PCUICAst.puinst p ] in
  PCUICSpine.spine_subst Σ Γ (PCUICAst.pparams p)
      (List.rev (PCUICAst.pparams p))
      (PCUICEnvironment.smash_context [] parctx) →
  wf_predicate mdecl idecl p →
  let p' := map_predicate id trans trans trans_local p in
  (case_predicate_context ci (trans_minductive_body mdecl) (trans_one_ind_body mdecl (inductive_ind ci) idecl) p') =
  (trans_local (PCUICCases.case_predicate_context ci mdecl idecl p)).
Proof.
  intros.
  rewrite /case_predicate_context /PCUICCases.case_predicate_context.
  rewrite /case_predicate_context_gen /PCUICCases.case_predicate_context_gen.
  rewrite /trans_local map_map2 map2_trans.
  rewrite -PCUICUnivSubstitutionConv.map2_map_r. f_equal.
  rewrite /p' /=. now rewrite forget_types_map_context.
  rewrite /pre_case_predicate_context_gen /inst_case_context.
  rewrite /PCUICCases.pre_case_predicate_context_gen /PCUICCases.inst_case_context.
  rewrite [map _ _](trans_subst_context (shiftnP (context_assumptions mdecl.(ind_params)) xpred0)
    (shiftnP #|Γ| xpred0)).
  rewrite -closedP_shiftnP on_free_vars_ctx_subst_instance.
  eapply (on_free_vars_ind_predicate_context H).
  now eapply inst_subslet, subslet_open in X.
  rewrite map_rev. f_equal.
  rewrite trans_subst_instance_ctx.
  rewrite trans_ind_predicate_context; pcuic.
Qed.

Lemma OnOne2All2i_OnOne2All {A B : Type} (l1 l2 : list A) (l3 : list B)
  (R1 : A → A → Type) (R2 : nat → B → A → Type) (n : nat) (R3 : B → A → A → Type) :
  OnOne2 R1 l1 l2 →
  All2i R2 n l3 l1 →
  (∀ (n0 : nat) (x y : A) (z : B), R1 x y → R2 n0 z x → R3 z x y ) → OnOne2All R3 l3 l1 l2.
Proof.
  induction 1 in n, l3 |- *; intros H; depelim H.
  intros H'. constructor. now eapply H'. eapply (All2i_length _ _ _ _ H).
  intros H'. constructor. now eapply IHX.
Qed.

Lemma trans_eq_binder_annot (Γ : list aname) Δ :
  Forall2 (fun na decl ⇒ eq_binder_annot na (decl_name decl)) Γ Δ →
  Forall2 (fun na decl ⇒ eq_binder_annot na (decl_name decl)) Γ (trans_local Δ).
Proof.
  induction 1; constructor; auto.
Qed.

Lemma map_context_trans Γ : map_context trans Γ = trans_local Γ.
Proof.
  rewrite /map_context /trans_local /trans_decl.
  eapply map_ext. intros []; reflexivity.
Qed.

Lemma trans_bcontext p br :
  (bcontext (trans_branch p (map_branch trans (map_context trans) br))) = smash_context [] (trans_local (bcontext br)).
Proof.
  rewrite /trans_branch.
  elim: is_assumption_context_spec ⇒ isass.
  rewrite smash_assumption_context //.
  now cbn.
Qed.

Lemma trans_bbody p br :
  (bbody (trans_branch p (map_branch trans (map_context trans) br))) =
  expand_lets (subst_context (List.rev (pparams p)) 0 (trans_local (bcontext br))@[puinst p ]) (trans (bbody br)).
Proof.
  rewrite /trans_branch.
  elim: is_assumption_context_spec ⇒ isass.
  { rewrite expand_lets_assumption_context //.
    now eapply assumption_context_subst_context, assumption_context_subst_instance. }
  cbn -[expand_lets].
  now cbn.
Qed.

Lemma OnOne2All_map2_map_all {A B I I'} {P} {i : list I} {l l' : list A} (g : B → I → I') (f : A → B) :
  OnOne2All (fun i x y ⇒ P (g (f x) i) (f x) (f y)) i l l' → OnOne2All P (map2 g (map f l) i) (map f l) (map f l').
Proof.
  induction 1; simpl; constructor; try congruence. len.
  now rewrite map2_length !map_length.
Qed.

Lemma wt_on_free_vars {cf} {Σ : global_env_ext} {wfΣ : wf Σ} {Γ t} : wt Σ Γ t → on_free_vars (shiftnP #|Γ | xpred0) t.
Proof.
  intros [T wt]. now eapply subject_is_open_term in wt.
Qed.

Ltac fuse_shifts :=
  match goal with
  [ H : is_true (on_free_vars (shiftnP 1 (shiftnP _ _)) _) |- _ ] ⇒
    rewrite → shiftnP_add in H; cbn in H
  end.

Ltac tofvs := repeat match goal with [ H : wt _ _ _ |- _ ] ⇒ apply wt_on_free_vars in H end;
  try inv_on_free_vars; repeat fuse_shifts.

#[local] Hint Extern 3 (is_true (_ && true)) ⇒ rewrite andb_true_r : pcuic.

Lemma skipn_map_length {A B} {n} {f : A → B} {l} : #|skipn n (map f l)| = #|skipn n l |.
Proof.
  now rewrite !List.skipn_length map_length.
Qed.

Lemma on_free_vars_ctx_cstr_branch_context {cf} {Σ : global_env_ext} {wfΣ : wf Σ} {c mdecl idecl cdecl} :
  declared_constructor Σ c mdecl idecl cdecl →
  on_free_vars_ctx (shiftnP (context_assumptions (ind_params mdecl)) xpred0)
    (cstr_branch_context c .1 mdecl cdecl).
Proof.
  intros. eapply closedn_ctx_on_free_vars. eapply (PCUICInstConv.closedn_ctx_cstr_branch_context H).
Qed.

Lemma typing_spine_wt {cf} {Σ : global_env_ext} {wfΣ : wf Σ} {args Γ x2 x3} :
  typing_spine Σ Γ x2 args x3 →
  All (wt Σ Γ) args.
Proof.
  intros sp.
  dependent induction sp; constructor; auto.
  now ∃ A.
Qed.

Lemma wt_mkApps_inv {cf} {Σ : global_env_ext} {wfΣ : wf Σ} {Γ f args} :
  wt Σ Γ (mkApps f args) → wt Σ Γ f × All (wt Σ Γ) args.
Proof.
  intros [ha tapp].
  eapply inversion_mkApps in tapp as [ty [tf targs]].
  split.
  - ∃ ty; eauto.
  - now eapply typing_spine_wt.
Qed.

Lemma red_expand_lets {cf} (Σ : global_env_ext) {wfΣ : wf Σ} Γ Δ t t' :
  Σ ;;; Γ ,,, Δ ⊢ t ⇝ t' →
  Σ ;;; Γ ,,, smash_context [] Δ ⊢ expand_lets Δ t ⇝ expand_lets Δ t'.
Proof.
  intros reds.
  rewrite /expand_lets /expand_lets_k. cbn.
  eapply (untyped_closed_red_subst (Γ := _ ,,, _) (Γ' := [])).
  eapply untyped_subslet_extended_subst; tea.
  len ⇒ /=. rewrite -shiftnP_add. rewrite foron_free_vars_extended_subst //.
  now move/PCUICAlpha.is_closed_context_app_right: (clrel_ctx reds).
  relativize #|Δ|. relativize (context_assumptions Δ).
  eapply weakening_closed_red; tea. all:try now len. 2:reflexivity.
  eapply is_closed_context_smash_end; fvs.
Qed.

From MetaCoq.PCUIC Require Import PCUICConfluence PCUICNormal.

Lemma red_context_rel_assumptions {cf} {Σ : global_env_ext} {Γ Δ Δ'} :
  red_context_rel Σ Γ Δ Δ' → context_assumptions Δ = context_assumptions Δ'.
Proof.
  induction 1; cbn; auto. destruct p; cbn; auto. lia.
Qed.

Lemma ws_cumul_pb_expand_lets {cf} {Σ : global_env_ext} {wfΣ : wf Σ} {Γ} {le} {Δ} {T T'} :
  Σ ;;; Γ ,,, Δ ⊢ T ≤[le ] T' →
  Σ ;;; Γ ,,, smash_context [] Δ ⊢ expand_lets Δ T ≤[le ] expand_lets Δ T'.
Proof.
  intros cum.
  pose proof (ws_cumul_pb_is_closed_context cum).
  eapply (weakening_ws_cumul_pb (Γ'' := smash_context [] Δ)) in cum; tea.
  rewrite /expand_lets /expand_lets_k.
  eapply (PCUICConversion.untyped_substitution_ws_cumul_pb (Γ'' := [])) in cum; tea. len in cum; tea.
  simpl.
  len.
  now eapply PCUICContexts.untyped_subslet_extended_subst.
  len. cbn. rewrite -shiftnP_add.
  rewrite foron_free_vars_extended_subst //.
  now move: H; rewrite on_free_vars_ctx_app ⇒ /andP[].
  now eapply is_closed_context_smash_end.
Qed.

Lemma red_terms_lift {cf} {Σ : global_env_ext} {wfΣ : wf Σ} {Γ Δ ts us} :
  is_closed_context (Γ ,,, Δ) →
  red_terms Σ Γ ts us →
  red_terms Σ (Γ ,,, Δ) (map (lift0 #|Δ |) ts) (map (lift0 #|Δ |) us).
Proof.
  intros r. solve_all.
  eapply (weakening_closed_red (Γ' := [])) ⇒ //.
Qed.

Lemma onfvs_app Γ Δ : is_closed_context (Γ ,,, Δ) →
  is_closed_context Γ ∧ on_free_vars_ctx (shiftnP #|Γ | xpred0) Δ.
Proof.
  now rewrite on_free_vars_ctx_app ⇒ /andP.
Qed.

Lemma untyped_subslet_ws_cumul_ctx_pb {cf} {Γ Γ' Δ Δ'} {s} :
  untyped_subslet (Γ ,,, Δ) s Γ' →
  untyped_subslet (Γ ,,, Δ') s Γ'.
Proof.
  induction 1; constructor; auto.
Qed.

Lemma weakening_is_closed_context Γ Δ :
  is_closed_context (Γ ,,, Δ) →
  is_closed_context (Γ ,,, smash_context [] Δ ,,, lift_context (context_assumptions Δ) 0 Δ).
Proof.
  move⇒ cl. rewrite on_free_vars_ctx_app.
  apply/andP; split.
  now eapply is_closed_context_smash_end.
  eapply on_free_vars_ctx_lift_context0.
  len ⇒ /=. rewrite -shiftnP_add addnP_shiftnP.
  now move/PCUICAlpha.is_closed_context_app_right: cl.
Qed.

Lemma red_context_rel_conv_extended_subst {cf} {Σ : global_env_ext} {wfΣ : wf Σ} {Γ Δ Δ'} :
  is_closed_context (Γ ,,, Δ) →
  is_closed_context (Γ ,,, Δ') →
  red_context_rel Σ Γ Δ Δ' →
  red_terms Σ (Γ ,,, smash_context [] Δ) (extended_subst Δ 0) (extended_subst Δ' 0) ×
  ws_cumul_ctx_pb_rel Conv Σ Γ (smash_context [] Δ) (smash_context [] Δ').
Proof.
  intros wfl wfr cum.
  assert (is_closed_context (Γ ,,, smash_context [] Δ)).
  { eapply is_closed_context_smash_end in wfl. eauto with fvs. }
  induction cum in |- *; simpl; auto.
  - split; constructor ⇒ //. constructor.
  - depelim p; simpl.
    move: wfl ⇒ /= /on_free_vars_ctx_snoc_ass_inv [] wfl clT.
    move: wfr ⇒ /= /on_free_vars_ctx_snoc_ass_inv [] wfr clT';
    specialize (IHcum wfl wfr) as [conv cum'];
    try assert (is_closed_context (Γ,,, smash_context [] Γ0)) by
      (rewrite /= smash_context_acc /= on_free_vars_ctx_snoc in H; now move/andP: H) ⇒ //.
    all:auto.
    × split; try constructor; auto.
      + eapply into_closed_red ⇒ //. cbn. len. now cbn.
      + rewrite !(lift_extended_subst _ 1).
        move: H.
        rewrite /= ![smash_context [_] _]smash_context_acc /= /map_decl /= ⇒ ha.
        eapply (red_terms_lift (Δ := [_])) ⇒ //.
      + now move/onfvs_app: H.
      + move: H; simpl; rewrite /= !(smash_context_acc _ [_]) /=;
        constructor; auto.
        apply cum'. rewrite /map_decl /=.
        constructor; auto.
        eapply into_closed_red in r; fvs.
        eapply red_ws_cumul_pb in r.
        eapply ws_cumul_pb_expand_lets in r; tea.
        etransitivity;tea. rewrite /expand_lets /expand_lets_k. simpl.
        rewrite -(length_of cum).
        rewrite -(red_context_rel_assumptions cum).
        move: (context_assumptions_smash_context [] Γ0); cbn ⇒ <-. simpl.
        change (Γ ,,, smash_context [] Γ0) with (Γ ,,, smash_context [] Γ0 ,,, []).
        eapply (untyped_substitution_ws_cumul_pb_subst_conv (Γ' := [])); tea.
        now eapply red_terms_ws_cumul_pb_terms in conv.
        3:eapply PCUICContexts.untyped_subslet_extended_subst.
        3:{ eapply untyped_subslet_ws_cumul_ctx_pb.
            now eapply untyped_subslet_extended_subst. }
        now eapply weakening_is_closed_context.
        cbn -[is_closed_context]. rewrite on_free_vars_ctx_app.
        apply/andP; split. now apply is_closed_context_smash_end.
        len ⇒ /=. rewrite -shiftnP_add. eapply on_free_vars_ctx_lift_context0.
        rewrite (red_context_rel_assumptions cum) addnP_shiftnP.
        now move/PCUICAlpha.is_closed_context_app_right: wfr.
        rewrite context_assumptions_smash_context /=.
        rewrite -[context_assumptions Γ0](smash_context_length []); cbn.
        relativize #|Γ0|.
        eapply is_open_term_lift.
        len. rewrite (All2_fold_length cum). now len in clT'. reflexivity.
    × move: wfl ⇒ /= /on_free_vars_ctx_snoc_def_inv ⇒ [] [] clΓ0 clb clT.
      move: wfr ⇒ /= /on_free_vars_ctx_snoc_def_inv ⇒ [] [] clΓ0' clb' clT'.
      specialize (IHcum clΓ0 clΓ0' ltac:(auto)) as [].
      split; auto.
      constructor; auto.
      len.
      eapply into_closed_red in r; fvs.
      eapply red_expand_lets in r; tea.
      etransitivity; tea. rewrite subst_context_nil.
      rewrite /expand_lets /expand_lets_k. simpl.
      rewrite -(length_of cum).
      rewrite -(red_context_rel_assumptions cum).
      move: (context_assumptions_smash_context [] Γ0); cbn ⇒ <-. simpl.
      change (smash_context [] Γ0 ++ Γ) with (Γ ,,, smash_context [] Γ0 ,,, []).
      cbn. rewrite smash_context_acc /=.
      change (smash_context [] Γ0 ++ Γ) with (Γ ,,, smash_context [] Γ0 ,,, []).
      eapply (closed_red_red_subst (Γ := _ ,,, _) (Γ' := [])); tea.
      2:{ eapply PCUICContexts.untyped_subslet_extended_subst. }
      { now eapply weakening_is_closed_context. }
      rewrite context_assumptions_smash_context /=.
      rewrite -[context_assumptions Γ0](smash_context_length []); cbn.
      relativize #|Γ0|.
      eapply is_open_term_lift.
      len. rewrite (All2_fold_length cum). now len in clb'. reflexivity.
Qed.

From MetaCoq.PCUIC Require Import PCUICSubstitution.

Lemma is_closed_context_subst Γ Γ' s Δ :
  is_closed_context (Γ ,,, Γ' ,,, Δ) →
  forallb (is_open_term Γ) s →
  #|s | = #|Γ'| →
  is_closed_context (Γ ,,, subst_context s 0 Δ).
Proof.
  intros clΓ cls slen.
  rewrite on_free_vars_ctx_app.
  rewrite -app_context_assoc on_free_vars_ctx_app in clΓ.
  move/andP: clΓ ⇒ [] → /=; rewrite on_free_vars_ctx_app ⇒ /andP[] o o'.
  apply on_free_vars_ctx_subst_context0 ⇒ //. now rewrite slen.
Qed.

Lemma red_expand_lets_ctx {cf} {Σ : global_env_ext} {wfΣ : wf Σ} {Γ Γ' Γ'' Δ s s' t} :
  is_closed_context (Γ ,,, Γ' ,,, Δ) →
  is_closed_context (Γ ,,, Γ'' ,,, Δ) →
  untyped_subslet Γ s Γ' →
  untyped_subslet Γ s' Γ'' →
  All2 (closed_red Σ Γ) s s' →
  is_open_term (Γ ,,, subst_context s 0 Δ) t →
  Σ ;;; Γ ,,, subst_context s 0 (smash_context [] Δ) ⊢
    (expand_lets (subst_context s 0 Δ) t ) ⇝
    (expand_lets (subst_context s' 0 Δ) t ).
Proof.
  intros wf wf' subs subs' reds ont.
  rewrite -smash_context_subst /= subst_context_nil.
  have cls : is_closed_context (Γ,,, subst_context s 0 Δ).
  { eapply is_closed_context_subst; tea. eapply closed_red_terms_open_left in reds. solve_all.
    now rewrite -(untyped_subslet_length subs') (All2_length reds). }
  have cls' : is_closed_context (Γ,,, subst_context s' 0 Δ).
  { eapply is_closed_context_subst; tea. eapply closed_red_terms_open_right in reds. solve_all.
    now rewrite -(untyped_subslet_length subs'). }
  etransitivity.
  eapply red_expand_lets; tea.
  eapply into_closed_red; tea. reflexivity.
  rewrite /expand_lets /expand_lets_k. len. cbn.
  eapply (closed_red_red_subst (Γ := _ ,,, _) (Γ' := [])); tea.
  3:{ eapply untyped_subslet_extended_subst. }
  eapply weakening_is_closed_context ⇒ //.
  eapply (red_context_rel_conv_extended_subst) ⇒ //.
  eapply red_ctx_rel_subst; tea. solve_all. apply X.
  solve_all. apply X.
  rewrite context_assumptions_subst.
  rewrite -[context_assumptions Δ](smash_context_length []).
  relativize #|smash_context [] _|. relativize #|Δ|.
  eapply is_open_term_lift. 2-3:now len. apply ont.
Qed.

Require Import PCUICSubstitution.

Lemma untyped_subslet_lift (Γ Δ : context) s Δ' :
  untyped_subslet Γ s Δ' →
  untyped_subslet (Γ ,,, Δ) (map (lift0 #|Δ |) s) (lift_context #|Δ | 0 Δ').
Proof.
  induction 1; rewrite ?lift_context_snoc /=; try constructor; auto.
  simpl.
  rewrite -(untyped_subslet_length X).
  rewrite distr_lift_subst. constructor; auto.
Qed.

Lemma OnOne2_All2i_All2 {A B} {P : A → A → Type} {Q R} {n} {l l' : list A} {l'' : list B} :
  OnOne2 P l l' →
  All2i Q n l'' l →
  (∀ n x y z, P x y → Q n z x → R x y ) →
  (∀ n x z, Q n z x → R x x ) →
  All2 R l l'.
Proof.
  intros o a. induction a in o, l' |- ×. depelim o.
  depelim o.
  - intros. constructor; eauto.
    clear -a X0.
    induction a; constructor; eauto.
  - intros. constructor.
    eapply X0; tea.
    eapply IHa; tea.
Qed.

From MetaCoq.PCUIC Require Import PCUICUnivSubstitutionConv.

Lemma OnOne2_All_OnOne2 {A} {P : A → A → Type} {Q R} l l' :
  OnOne2 P l l' →
  All Q l →
  (∀ x y, Q x → P x y → R x y ) →
  OnOne2 R l l'.
Proof.
  induction 1; intros H; depelim H; intros IH; constructor; eauto.
Qed.

Lemma OnOne2_All_All2 {A} {P : A → A → Type} {Q R} l l' :
  OnOne2 P l l' →
  All Q l →
  (∀ x y, Q x → P x y → R x y ) →
  (∀ x, Q x → R x x ) →
  All2 R l l'.
Proof.
  induction 1; intros H; depelim H; intros IH; constructor; eauto.
  clear -H X; solve_all.
Qed.

Lemma All2i_map_right_inv {A B C} {P : nat → A → B → Type} {f : C → B} n (l : list A) l' :
  All2i P n l (map f l') →
  All2i (fun n x y ⇒ P n x (f y)) n l l'.
Proof.
  induction l' in n, l |- *; cbn; intros h; depelim h; constructor; auto.
Qed.

Lemma All2i_map_left_inv {A B C} {P : nat → A → B → Type} {f : C → A} n l l' :
  All2i P n (map f l) l' →
  All2i (fun n x y ⇒ P n (f x) y) n l l'.
Proof.
  induction l in n, l' |- *; cbn; intros h; depelim h; constructor; auto.
Qed.

Lemma trans_is_closed_context Γ : is_closed_context Γ → is_closed_context (map_context trans Γ).
Proof.
  move⇒ cl; eapply on_free_vars_ctx_impl; [|eapply (on_free_vars_ctx_trans 0)].
  intros i. rewrite /closedP; now cbn.
  now rewrite closedP_shiftnP shiftnP0.
Qed.

Lemma on_free_vars_ind_params {cf} {Σ : global_env_ext} {wfΣ : wf Σ} {P ind mdecl idecl u} :
  declared_inductive Σ ind mdecl idecl →
  on_free_vars_ctx P (ind_params mdecl )@[u ].
Proof.
  intros decl.
  eapply on_free_vars_ctx_impl; [|eapply closedn_ctx_on_free_vars]; revgoals.
  rewrite closedn_subst_instance_context.
  eapply (declared_inductive_closed_params decl).
  intros i; rewrite shiftnP0 //.
Qed.

Lemma shiftnP_mon n n' i : n ≤ n' → shiftnP n xpred0 i → shiftnP n' xpred0 i.
Proof.
  rewrite /shiftnP.
  repeat nat_compare_specs; cbn; auto.
Qed.

Lemma is_closed_context_cstr_branch_context {cf} {Σ : global_env_ext} {wfΣ : wf Σ} {Γ ind mdecl idecl cdecl u} :
  declared_constructor Σ ind mdecl idecl cdecl →
  is_closed_context Γ →
  is_closed_context (Γ ,,, (smash_context [] (ind_params mdecl))@[u ] ,,, (cstr_branch_context ind .1 mdecl cdecl )@[u ]).
Proof.
  intros declc clΓ.
  rewrite -app_context_assoc on_free_vars_ctx_app clΓ /=.
  rewrite on_free_vars_ctx_app.
  apply/andP; split.
  rewrite subst_instance_smash.
  eapply on_free_vars_ctx_smash ⇒ //. apply (on_free_vars_ind_params declc).
  len. cbn.
  rewrite on_free_vars_ctx_subst_instance.
  eapply on_free_vars_ctx_impl; [|eapply (on_free_vars_ctx_cstr_branch_context declc)].
  intros i. rewrite shiftnP_add. eapply shiftnP_mon.
  move: (context_assumptions_bound (ind_params mdecl)). lia.
Qed.

Lemma trans_untyped_subslet {cf} {Σ : global_env_ext} {wfΣ : wf Σ} {Γ s Δ} :
  wf_local Σ (Γ ,,, Δ ) →
  All (wt Σ Γ) s →
  untyped_subslet Γ s Δ →
  untyped_subslet (trans_local Γ) (map trans s) (trans_local Δ).
Proof.
  induction 3 in |- *; cbn; try constructor; auto.
  cbn. depelim X. now depelim X0.
  depelim X. depelim X0.
  rewrite (trans_subst (shiftnP #|Γ ,,, Δ| xpred0) (shiftnP #|Γ| xpred0)).
  red in l0. now eapply subject_is_open_term in l0. solve_all. now eapply wt_on_free_vars.
  constructor ; auto.
Qed.

Lemma untyped_subslet_length Γ s s' Δ :
  untyped_subslet Γ s Δ → #|s | = #|s'| → assumption_context Δ → untyped_subslet Γ s' Δ.
Proof.
  induction 1 in s' |- *; cbn; destruct s' ⇒ /= //. constructor.
  intros [=]. constructor ; auto. eapply IHX; auto. now depelim H.
  intros. elimtype False; depelim H0.
Qed.

Lemma wf_local_ind_params_weaken {cf} {Σ : global_env_ext} {wfΣ : wf Σ} {Γ} {ind mdecl u} :
  declared_minductive Σ ind mdecl →
  wf_local Σ Γ →
  consistent_instance_ext Σ (ind_universes mdecl) u →
  wf_local Σ (Γ ,,, (ind_params mdecl )@[u ]).
Proof.
  intros decli wfΓ cu.
  eapply weaken_wf_local ⇒ //.
  now eapply on_minductive_wf_params.
Qed.

Definition cf' cf :=
  {| check_univs := cf.(@check_univs);
     prop_sub_type := cf.(@prop_sub_type);
     indices_matter := cf.(@indices_matter);
     lets_in_constructor_types := false |}.

Notation wf_trans Σ := (@wf (cf' _) (trans_global_env Σ.1)).
Notation wf_ext_trans Σ := (@wf_ext (cf' _) (trans_global Σ)).

Lemma trans_red1 {cf} (Σ : global_env_ext) {wfΣ : wf Σ} {wfΣ' : wf_trans Σ} Γ T U :
  red1 Σ Γ T U →
  wt Σ Γ T →
  red (trans_global Σ) (trans_local Γ) (trans T) (trans U).
Proof.
  induction 1 using red1_ind_all; simpl in *; intros wt;
    match goal with
    | |- context [tCase _ _ _ _] ⇒ idtac
    | |- context [tFix _ _] ⇒ idtac
    | |- context [tCoFix _ _] ⇒ idtac
    | _ ⇒ eapply wt_inv in wt; tea; cbn in wt; repeat outtimes
    end;
    try solve [econstructor; eauto].

  - simpl. tofvs.
    rewrite (trans_subst_ctx Γ) /=; pcuic. eapply red1_red; constructor.

  - destruct wt. tofvs. rewrite (trans_subst_ctx Γ); pcuic. repeat constructor.

  - destruct nth_error eqn:Heq ⇒ //. simpl in H. noconf H.
    simpl. destruct c; noconf H ⇒ //.
    rewrite (trans_lift _ (shiftnP #|skipn (S i) Γ| xpred0)); eauto.
    eapply nth_error_All_local_env in wt0; tea. cbn in wt0.
    now eapply subject_is_open_term.
    do 2 constructor. now rewrite nth_error_map Heq.

  - pose proof (wt_on_free_vars wt).
    inv_on_free_vars.
    destruct wt as [s Hs].
    eapply inversion_Case in Hs as [mdecl [idecl [decli [indices [[] e]]]]].
    epose proof (PCUICValidity.inversion_mkApps scrut_ty) as [? [hc hsp]]; tea.
    eapply inversion_Construct in hc as (mdecl'&idecl'&cdecl&wfΓ&declc&cu&tyc); tea.
    destruct (declared_inductive_inj decli (proj1 declc)) as [-> ->]. 2:auto.
    rewrite trans_mkApps /=.
    have lenskip : #|skipn (ci_npar ci) (map trans args)| =
      context_assumptions (cstr_args cdecl).
    { destruct (Construct_Ind_ind_eq _ scrut_ty declc) as [[? e'] _].
      rewrite skipn_length; len; lia. }
    eapply All2i_nth_error_r in brs_ty; tea.
    destruct brs_ty as [cdecl' [Hcdecl' [bctxeq [wfbrctx [hbody hbodyty]]]]].
    rewrite (proj2 declc) in Hcdecl'. noconf Hcdecl'.
    have lenbctx : context_assumptions (cstr_args cdecl) = context_assumptions (bcontext br).
    { rewrite (alpha_eq_context_assumptions _ _ bctxeq).
      rewrite cstr_branch_context_assumptions. lia. }
    relativize (trans (iota_red _ _ _ _)).
    eapply red1_red; eapply red_iota; tea; eauto. all:auto.
    × rewrite !nth_error_map H; reflexivity.
    × rewrite trans_bcontext (context_assumptions_smash_context []) /= context_assumptions_map.
      len. eauto.
    × rewrite /iota_red. rewrite skipn_map_length in lenskip.
      have oninst : on_free_vars_ctx (shiftnP #|Γ| xpred0) (inst_case_branch_context p br).
      { rewrite -(PCUICCasesContexts.inst_case_branch_context_eq bctxeq).
        eapply typing_wf_local in hbody. eapply wf_local_closed_context in hbody.
        rewrite → on_free_vars_ctx_app in hbody.
        move/andP: hbody ⇒ [] //. }
      have onb : on_free_vars (shiftnP #|inst_case_branch_context p br| (shiftnP #|Γ| xpred0)) (bbody br).
      { rewrite -(PCUICCasesContexts.inst_case_branch_context_eq bctxeq).
        eapply subject_is_open_term in hbody. len in hbody. rewrite shiftnP_add //. }
      rewrite (trans_subst_ctx Γ).
      { len. rewrite lenskip.
        rewrite -shiftnP_add.
        eapply on_free_vars_expand_lets_k ⇒ //.
        rewrite /inst_case_branch_context /inst_case_context.
        rewrite context_assumptions_subst_context context_assumptions_subst_instance. lia. }
      { rewrite forallb_rev forallb_skipn //.
        rewrite on_free_vars_mkApps in p3. move: p3 ⇒ /= //. }
      rewrite map_rev map_skipn. f_equal.
      rewrite (trans_expand_lets (shiftnP #|Γ| xpred0)) //.
      cbn -[expand_lets].
      rewrite expand_lets_assumption_context.
      { apply assumption_context_subst_context.
        apply assumption_context_subst_instance.
        rewrite trans_bcontext.
        apply smash_context_assumption_context ⇒ //.
        constructor. }
      f_equal.
      rewrite /inst_case_branch_context /inst_case_context.
      rewrite (trans_subst_context (shiftnP (#|Γ| + #|ind_params mdecl|) xpred0) (shiftnP #|Γ| xpred0)).
      { rewrite on_free_vars_ctx_subst_instance.
        eapply alpha_eq_on_free_vars_ctx; [symmetry; tea|].
        eapply on_free_vars_ctx_impl; [|eapply (on_free_vars_ctx_cstr_branch_context declc)].
        intros i. rewrite /shiftnP. rewrite !orb_false_r.
        move/Nat.ltb_lt ⇒ H'. apply Nat.ltb_lt.
        pose proof (context_assumptions_bound (ind_params mdecl)). lia. }
      { rewrite [on_free_vars_terms _ _]forallb_rev //. }
      rewrite map_rev. f_equal.
      rewrite trans_subst_instance_ctx //.
      now rewrite trans_bbody.

  - simpl. rewrite !trans_mkApps /=.
    eapply wt_mkApps_inv in wt as [wtf wtargs].
    unfold is_constructor in H0.
    destruct nth_error eqn:hnth.
    pose proof (nth_error_Some_length hnth).
    destruct args. simpl. elimtype False; cbn in H1. lia.
    cbn -[mkApps].
    eapply red1_red, red_fix.
    apply (trans_unfold_fix (shiftnP #|Γ| xpred0)); eauto.
    now eapply wt_on_free_vars in wtf.
    eapply (trans_is_constructor (t0 :: args)).
    now rewrite /is_constructor hnth.
    discriminate.

  - rewrite trans_mkApps.
    rewrite !trans_mkApps; eauto with wf.
    eapply wt_inv in wt. cbn in wt.
    destruct wt as [wtpars [idecl [cdecl []]]].
    eapply wt_mkApps_inv in w2 as [].
    apply (trans_unfold_cofix (shiftnP #|Γ| xpred0)) in H; eauto with wf.
    eapply red1_red, red_cofix_case; eauto.
    now eapply wt_on_free_vars in w2.

  - rewrite !trans_mkApps.
    eapply wt_inv in wt. cbn in wt.
    eapply wt_mkApps_inv in wt as [].
    apply (trans_unfold_cofix (shiftnP #|Γ| xpred0)) in H; eauto with wf.
    eapply red1_red, red_cofix_proj; eauto.
    now eapply wt_on_free_vars in w.

  - rewrite trans_subst_instance. eapply red1_red; econstructor.
    apply (trans_declared_constant _ c decl H).
    destruct decl. now simpl in *; subst cst_body0.

  - rewrite trans_mkApps; eauto with wf.
    simpl. eapply red1_red; constructor; now rewrite nth_error_map H.

  - eapply red_abs; eauto.
  - eapply red_abs; eauto.
  - destruct wt as []; eapply red_letin; eauto.
  - destruct wt as []; eapply red_letin; eauto.
  - destruct wt as []; eapply red_letin; eauto.
  - eapply wt_inv in wt as [hpars [mdecl [idecl []]]].
    eapply OnOne2_All_mix_left in X; tea.
    relativize (map_predicate id _ _ _ (set_pparams _ _)).
    eapply red_case. 5:reflexivity. all:try reflexivity.
    cbn.
    eapply OnOne2_All2. eapply OnOne2_map.
    2:intros x y h; exact h. 2:reflexivity.
    eapply OnOne2_All_OnOne2; tea. cbv beta.
    intros x y wtt [[r IH] wt]. specialize (IH wt).
    red. apply IH.
    rewrite /trans_branch. cbn.
    eapply All2_map. cbn. eapply All2_map, All_All2_refl.
    eapply All2i_nth_hyp in a0.
    eapply All2i_All_right; tea. cbv beta. clear a0.
    intros ctor cdecl br [hnth [wfbr eqbctx wfbctx eqinst wtb]].
    elim: is_assumption_context_spec ⇒ isass.
    { split ⇒ //. }
    split ⇒ //. cbn [bcontext bbody map_branch]. rewrite /id.
    rewrite (subst_instance_smash _ _ []) /=.
    eapply (red_expand_lets_ctx (cf := cf' cf) (Σ := trans_global Σ)
      (Γ' := (trans_local (smash_context [] (ind_params mdecl))@[puinst p]))
      (Γ'' := (trans_local (smash_context [] (ind_params mdecl))@[puinst p]))).
    × eapply alpha_eq_on_free_vars_ctx.
      eapply All2_app; [|reflexivity].
      eapply alpha_eq_subst_instance.
      eapply alpha_eq_trans. symmetry. exact eqbctx.
      rewrite - !trans_subst_instance_ctx -!trans_local_app.
      rewrite -[_ ++ _]trans_local_app.
      eapply trans_is_closed_context.
      have declc : declared_constructor Σ (ci, ctor) mdecl idecl cdecl.
      { split; tea. }
      eapply (is_closed_context_cstr_branch_context declc).
      destruct w2 as [? ? % typing_closed_ctx]; eauto.
    × eapply alpha_eq_on_free_vars_ctx.
      eapply All2_app; [|reflexivity].
      eapply alpha_eq_subst_instance.
      eapply alpha_eq_trans. symmetry. exact eqbctx.
      rewrite - !trans_subst_instance_ctx -!trans_local_app.
      rewrite -[_ ++ _]trans_local_app.
      eapply trans_is_closed_context.
      have declc : declared_constructor Σ (ci, ctor) mdecl idecl cdecl.
      { split; tea. }
      eapply (is_closed_context_cstr_branch_context declc).
      destruct w2 as [? ? % typing_closed_ctx]; eauto.
    × rewrite -map_rev.
      eapply trans_untyped_subslet.
      { rewrite subst_instance_smash. eapply wf_local_smash_end.
        eapply wf_local_ind_params_weaken; tea. exact d. exact w2. }
      { solve_all. }
      rewrite subst_instance_smash.
      eapply subslet_untyped_subslet; exact s.
    × rewrite -map_rev.
      eapply trans_untyped_subslet.
      { rewrite subst_instance_smash. eapply wf_local_smash_end.
        eapply wf_local_ind_params_weaken; tea. exact d. exact w2. }
      { solve_all.
        eapply spine_subst_wt_terms in s.
        solve_all. eapply OnOne2_impl_All_r; tea.
        2:solve_all. cbv beta; intros x y wtx [[Hr _]].
        eapply wt_red; tea. }
      eapply untyped_subslet_length.
      rewrite subst_instance_smash. exact s. len.
      eapply (OnOne2_length X).
      pcuic.
    × eapply All2_rev. eapply All2_map.
      eapply OnOne2_All_All2; tea; cbv beta.
      intros x y wtx [[r Hr] wt].
      specialize (Hr wt).
      destruct wtx. eapply into_closed_red ⇒ //.
      eapply typing_closed_ctx in t; tea.
      now eapply trans_is_closed_context.
      eapply trans_on_free_vars. len.
      now eapply subject_is_open_term in t.
      intros x []. eapply into_closed_red. reflexivity.
      eapply typing_closed_ctx in t. now eapply trans_is_closed_context. auto.
      eapply subject_is_open_term in t. eapply trans_on_free_vars. now len.
    × len. destruct wtb. cbn in t.
      eapply subject_is_open_term in t.
      len in t. rewrite (case_branch_context_length wfbr) in t.
      now eapply trans_on_free_vars.
  - eapply wt_inv in wt as [hpars [mdecl [idecl []]]].
    eapply red_case_p.
    symmetry in a. rewrite (inst_case_predicate_context_eq a) in w1.
    specialize (IHX w1).
    rewrite -(inst_case_predicate_context_eq a) in IHX.
    eapply alpha_eq_trans in a.
    rewrite trans_ind_predicate_context in a.
    { eapply closed_ctx_is_closed_context, declared_inductive_closed_params; tea. }
    { epose proof (declared_inductive_closed_indices _ _ _ d).
      now eapply closedn_ctx_on_free_vars in H. }
    set (p' := map_predicate id trans _ _ p).
    rewrite -(inst_case_predicate_context_eq (p:=p') a).
    rewrite (trans_case_predicate_context d c0 s w).
    now rewrite -trans_local_app.

  - eapply wt_inv in wt as [hpars [mdecl [idecl []]]].
    eapply red_case_c; eauto.

  - pose proof (wt_on_free_vars wt). inv_on_free_vars.
    eapply forallb_All in p4.
    eapply wt_inv in wt as [hpars [mdecl [idecl []]]].
    eapply red_case_brs.
    do 2 eapply All2_map.
    eapply All2i_All_mix_right in a0; tea.
    eapply OnOne2_All2i_All2; tea; cbv beta.
    intros _ br br' cdecl [[hred ih] eqctx].
    intros [[] onfvs].
    intros ctx. split ⇒ //. 2:{ rewrite !trans_bcontext. cbn. now rewrite eqctx. }
    2:{ intros; split; reflexivity. }
    rewrite -{1}(PCUICCasesContexts.inst_case_branch_context_eq a1) in ih.
    specialize (ih w5).
    rewrite trans_local_app in ih.
    cbn -[expand_lets].
    rewrite !trans_bcontext !trans_bbody.
    rewrite (subst_instance_smash _ _ []).
    rewrite -(smash_context_subst []) /=. len. rewrite subst_context_nil /id.
    rewrite -eqctx.
    eapply (red_expand_lets (cf := cf' cf) (trans_global Σ)). cbn.
    rewrite /inst_case_branch_context in ih.
    rewrite /inst_case_context in ih.
    rewrite (trans_subst_context (shiftnP #|pparams p| xpred0) (shiftnP #|Γ| xpred0)) // in ih.
    { rewrite on_free_vars_ctx_subst_instance //.
      move/andP: onfvs. rewrite test_context_k_closed_on_free_vars_ctx.
      now rewrite closedP_shiftnP. }
    { rewrite [on_free_vars_terms _ _]forallb_rev. solve_all. }
    rewrite map_rev in ih.
    rewrite trans_subst_instance_ctx in ih.
    move: ih.
    rewrite -!trans_subst_instance_ctx.
    rewrite -!map_rev -!(trans_subst_context (closedP #|pparams p| xpredT) (shiftnP #|Γ| xpred0)).
    { move/andP: onfvs ⇒ [] onctx _. rewrite test_context_k_closed_on_free_vars_ctx in onctx.
      now rewrite on_free_vars_ctx_subst_instance. }
    { rewrite /on_free_vars_terms forallb_rev. solve_all. }
    rewrite -!trans_local_app.
    intros r; eapply into_closed_red ⇒ //.
    { eapply trans_is_closed_context.
      rewrite -[SE.subst_context _ _ _](PCUICCasesContexts.inst_case_branch_context_eq (p:=p) a1).
      destruct w5 as [? wt]. now eapply typing_closed_ctx in wt. }
    { eapply trans_on_free_vars.
      move/andP: onfvs ⇒ [] onctx onb. len.
      now rewrite -shiftnP_add. }

  - eapply red_proj_c; eauto.
  - eapply red_app; eauto.
  - eapply red_app; eauto.
  - eapply red_prod; eauto.
  - eapply red_prod; eauto.
  - eapply red_fix_congr.
    eapply All2_map.
    eapply wt_inv in wt. cbn in wt.
    eapply OnOne2_All_mix_left in X; tea.
    eapply OnOne2_All2; tea; cbv beta.
    intros; intuition auto. cbn. noconf b0. rewrite H0; reflexivity.
    cbn. congruence.
    intros. repeat split; reflexivity.

  - eapply red_fix_congr.
    eapply All2_map.
    pose proof (wt_on_free_vars wt).
    eapply wt_inv in wt. cbn in wt.
    eapply OnOne2_All_mix_left in X; tea.
    eapply OnOne2_All2; tea; cbv beta.
    intros; intuition auto. cbn. noconf b0. rewrite H1; reflexivity.
    cbn.
    rewrite -(trans_fix_context (shiftnP #|Γ| xpred0) _ idx) //.
    now rewrite trans_local_app in X0. cbn; congruence.
    intros. repeat split; reflexivity.

  - eapply red_cofix_congr.
    eapply All2_map.
    eapply wt_inv in wt. cbn in wt.
    eapply OnOne2_All_mix_left in X; tea.
    eapply OnOne2_All2; tea; cbv beta.
    intros; intuition auto. cbn. noconf b0. rewrite H0; reflexivity.
    cbn. congruence.
    intros. repeat split; reflexivity.

  - eapply red_cofix_congr.
    pose proof (wt_on_free_vars wt).
    eapply All2_map.
    eapply wt_inv in wt. cbn in wt.
    eapply OnOne2_All_mix_left in X; tea.
    eapply OnOne2_All2; tea; cbv beta.
    intros; intuition auto. cbn. noconf b0. rewrite H1; reflexivity.
    cbn.
    rewrite -(trans_fix_context (shiftnP #|Γ| xpred0) _ idx) //.
    now rewrite trans_local_app in X0. cbn; congruence.
    intros. repeat split; reflexivity.
Qed.

Lemma trans_R_global_instance {Σ : global_env} Re Rle gref napp u u' :
  R_global_instance Σ Re Rle gref napp u u' →
  R_global_instance (trans_global_env Σ) Re Rle gref napp u u'.
Proof.
  unfold PCUICEquality.R_global_instance, PCUICEquality.global_variance.
  destruct gref; simpl; auto.
  - unfold S.lookup_inductive, S.lookup_minductive.
    unfold lookup_inductive, lookup_minductive.
    rewrite trans_lookup. destruct SE.lookup_env ⇒ //; simpl.
    destruct g ⇒ /= //. rewrite nth_error_mapi.
    destruct nth_error ⇒ /= //.
    rewrite trans_destr_arity.
    destruct PCUICAst.destArity as [[ctx ps]|] ⇒ /= //.
    now rewrite context_assumptions_map.
  - unfold S.lookup_constructor, S.lookup_inductive, S.lookup_minductive.
    unfold lookup_constructor, lookup_inductive, lookup_minductive.
    rewrite trans_lookup. destruct SE.lookup_env ⇒ //; simpl.
    destruct g ⇒ /= //. rewrite nth_error_mapi.
    destruct nth_error ⇒ /= //.
    rewrite nth_error_map.
    destruct nth_error ⇒ /= //.
Qed.

Lemma trans_eq_context_gen_eq_binder_annot Γ Δ :
  eq_context_gen eq eq Γ Δ →
  All2 eq_binder_annot (map decl_name (trans_local Γ)) (map decl_name (trans_local Δ)).
Proof.
  move/All2_fold_All2.
  intros; do 2 eapply All2_map. solve_all.
  destruct X; cbn; auto.
Qed.

Lemma trans_eq_context_gen Γ Δ :
  eq_context_gen eq eq Γ Δ →
  eq_context_gen eq eq (trans_local Γ) (trans_local Δ).
Proof.
  move/All2_fold_All2 ⇒ e. apply All2_fold_All2.
  eapply All2_map. solve_all.
  destruct X; cbn; subst; constructor; auto.
Qed.

Lemma eq_context_gen_extended_subst {Γ Δ n} :
  eq_context_gen eq eq Γ Δ →
  extended_subst Γ n = extended_subst Δ n.
Proof.
  induction 1 in n |- *; cbn; auto.
  destruct p; subst; cbn. f_equal; auto.
  rewrite IHX.
  now rewrite (PCUICConfluence.eq_context_gen_context_assumptions X).
Qed.

Lemma eq_context_gen_smash_context {Γ Δ} :
  eq_context_gen eq eq Γ Δ →
  eq_context_gen eq eq (smash_context [] Γ) (smash_context [] Δ).
Proof.
  induction 1; try constructor.
  rewrite (smash_context_app [] [d]) smash_context_acc.
  rewrite (smash_context_app [] [d']) (smash_context_acc Γ').
  cbn. destruct p; subst; cbn. eapply All2_fold_All2.
  eapply All2_app. 2:now eapply All2_fold_All2.
  rewrite !lift_context_snoc /=.
  rewrite (All2_fold_length X). repeat constructor; cbn; auto.
  rewrite (eq_context_gen_extended_subst X).
  now rewrite (PCUICConfluence.eq_context_gen_context_assumptions X).
  eapply All2_fold_app ⇒ //.
  constructor.
Qed.

Lemma eq_context_upto_context_assumptions {Σ : global_env} {Re Rle} {Γ Δ} :
  eq_context_upto Σ Re Rle Γ Δ →
  context_assumptions Γ = context_assumptions Δ.
Proof.
  induction 1; cbn; auto.
  destruct p; subst; cbn; auto. f_equal; auto.
Qed.

Lemma eq_term_upto_univ_expand_lets {cf} {Σ : global_env} {Re Rle Γ Δ t u napp} :
  subrelation Re Rle →
  eq_context_upto Σ Re Rle Γ Δ →
  eq_term_upto_univ_napp Σ Re Rle napp t u →
  eq_term_upto_univ_napp Σ Re Rle napp (expand_lets Γ t) (expand_lets Δ u).
Proof.
  intros subr eqctx eqt.
  rewrite /expand_lets /expand_lets_k.
  eapply eq_term_upto_univ_substs ⇒ //.
  rewrite (eq_context_upto_length eqctx).
  rewrite (eq_context_upto_context_assumptions eqctx).
  now eapply eq_term_upto_univ_lift.
  apply (PCUICConfluence.eq_context_extended_subst eqctx).
Qed.

Lemma trans_eq_term_upto_univ {cf} {Σ : global_env} {Re Rle t u napp} :
  Reflexive Re → Reflexive Rle →
  Transitive Re → SubstUnivPreserving Re →
  subrelation Re Rle →
  PCUICEquality.eq_term_upto_univ_napp Σ Re Rle napp t u →
  eq_term_upto_univ_napp (trans_global_env Σ) Re Rle napp (trans t) (trans u).
Proof.
  intros hre hrle hret hres hsub e.
  induction t using term_forall_list_ind in Rle, hrle, hsub, napp, u, e |- ×.
  all: invs e; cbn.
  all: try solve [ constructor ; auto ].
  all: try solve [
    repeat constructor ;
    match goal with
    | ih : ∀ Rle u (napp : nat), _ |- _ ⇒
      eapply ih ; eauto using subrelation_refl
    end
  ].
  1,2,3,4,5,6: try solve [ constructor; solve_all; eauto using subrelation_refl ].
  all: try solve [ constructor; now eapply trans_R_global_instance ].
  - destruct X1 as [Hpars [Huinst [Hctx Hret]]].
    destruct X as [IHpars [IHctx IHret]].
    constructor; cbn; auto. solve_all.
    constructor; cbn. solve_all.
    1,3:eauto using subrelation_refl.
    repeat split; eauto using subrelation_refl.
    rewrite !map_context_trans.
    now eapply trans_eq_context_gen.
    red in X0. do 2 apply All2_map.
    eapply All2_All_mix_left in X3; tea.
    eapply All2_impl; tea; cbv beta.
    intuition auto.
    rewrite !trans_bcontext.
    eapply eq_context_gen_smash_context.
    now eapply trans_eq_context_gen in a.
    rewrite !trans_bbody.
    apply eq_term_upto_univ_expand_lets; eauto; tc.
    apply eq_context_upto_subst_context; eauto; tc.
    rewrite /id.
    eapply PCUICConfluence.eq_context_upto_univ_subst_instance'; tc; auto.
    cbn.
    now eapply trans_eq_context_gen.
    cbn. eapply All2_rev. solve_all. eauto using subrelation_refl.
    cbn. eauto using subrelation_refl.
  - constructor. solve_all; eauto using subrelation_refl.
  - constructor; solve_all; eauto using subrelation_refl.
Qed.

Lemma trans_compare_term {cf} {Σ : global_env} {pb ϕ T U} :
  compare_term pb Σ ϕ T U →
  compare_term (H:=cf' cf) pb (trans_global_env Σ) ϕ (trans T) (trans U).
Proof.
  eapply trans_eq_term_upto_univ ; eauto; tc.
Qed.

Lemma trans_leq_term {cf} {Σ : global_env} ϕ T U :
  PCUICEquality.leq_term Σ ϕ T U →
  @compare_term (cf' cf) Cumul (trans_global_env Σ) ϕ (trans T) (trans U).
Proof.
  eapply trans_eq_term_upto_univ; eauto; tc.
Qed.

From MetaCoq.PCUIC Require Import PCUICContextConversion.

Lemma wt_red1_wt {cf} {Σ} {wfΣ : wf Σ} {Γ t u} :
  wt Σ Γ t → red1 Σ Γ t u → wt Σ Γ u.
Proof.
  intros [s ht] r.
  ∃ s. eapply subject_reduction1; tea.
Qed.

Section wtcumul.
  Import PCUICAst PCUICTyping PCUICEquality.
  Context {cf : checker_flags}.
  Record wt_red1 {cf} (Σ : PCUICEnvironment.global_env_ext) (Γ : PCUICEnvironment.context) T U :=
  { wt_red1_red1 : PCUICReduction.red1 Σ Γ T U;
    wt_red1_dom : wt Σ Γ T;
    wt_red1_codom : wt Σ Γ U }.

  Reserved Notation " Σ ;;; Γ |-- t <=[ le ] u " (at level 50, Γ, le, t, u at next level).

  Inductive wt_cumul_pb (pb : conv_pb) (Σ : global_env_ext) (Γ : context) : term → term → Type :=
  | wt_cumul_refl t u : compare_term pb Σ .1 (global_ext_constraints Σ) t u → Σ ;;; Γ |-- t <=[pb ] u
  | wt_cumul_red_l t u v : wt_red1 Σ Γ t v → Σ ;;; Γ |-- v <=[pb ] u → Σ ;;; Γ |-- t <=[pb ] u
  | wt_cumul_red_r t u v : Σ ;;; Γ |-- t <=[pb ] v → wt_red1 Σ Γ u v → Σ ;;; Γ |-- t <=[pb ] u
  where " Σ ;;; Γ |-- t <=[ pb ] u " := (wt_cumul_pb pb Σ Γ t u) : type_scope.

  Definition wt_cumul := wt_cumul_pb Cumul.
  Definition wt_conv := wt_cumul_pb Conv.

  Lemma cumul_decorate (Σ : global_env_ext) {wfΣ : wf Σ} Γ T U :
    isType Σ Γ T → isType Σ Γ U →
    cumulAlgo Σ Γ T U →
    wt_cumul_pb Cumul Σ