Library MetaCoq.PCUIC.PCUICParallelReductionConfluence

From Coq Require CMorphisms.
From MetaCoq.Template Require Import config utils.
From MetaCoq.PCUIC Require Import PCUICAst PCUICOnOne PCUICAstUtils PCUICTactics PCUICSize PCUICLiftSubst
     PCUICSigmaCalculus PCUICUnivSubst PCUICTyping PCUICReduction
     PCUICReflect PCUICInduction PCUICClosed PCUICClosedConv PCUICClosedTyp PCUICDepth PCUICOnFreeVars
     PCUICRenameDef PCUICRenameConv PCUICInstDef PCUICInstConv PCUICWeakeningConv PCUICWeakeningTyp
     PCUICViews PCUICParallelReduction.

Require Import ssreflect ssrbool.
Require Import Morphisms CRelationClasses.
From Equations Require Import Equations.

Add Search Blacklist "pred1_rect".
Add Search Blacklist "_equation_".

Local Open Scope sigma_scope.
Local Set Keyed Unification.

Ltac solve_discr := (try (progress (prepare_discr; finish_discr; cbn [mkApps] in × )));
  try discriminate.

Section FoldFix.
  Context (rho : context term term).
  Context (Γ : context).

  Fixpoint fold_fix_context acc m :=
    match m with
  | []acc
    | def :: fixd
      fold_fix_context (vass def.(dname) (lift0 #|acc| (rho Γ def.(dtype))) :: acc) fixd
    end.
End FoldFix.

Lemma fold_fix_context_length f Γ l m : #|fold_fix_context f Γ l m| = #|m| + #|l|.
Proof.
  induction m in l |- *; simpl; auto. rewrite IHm. simpl. auto with arith.
Qed.

Lemma fix_context_gen_assumption_context k Γ : assumption_context (fix_context_gen k Γ).
Proof.
  rewrite /fix_context_gen. revert k.
  induction Γ using rev_ind.
  constructor. intros.
  rewrite mapi_rec_app /= List.rev_app_distr /=. constructor.
  apply IHΓ.
Qed.

Lemma fix_context_assumption_context m : assumption_context (fix_context m).
Proof. apply fix_context_gen_assumption_context. Qed.

Lemma nth_error_assumption_context Γ n d :
  assumption_context Γ nth_error Γ n = Some d
  decl_body d = None.
Proof.
  intros H; induction H in n, d |- × ; destruct n; simpl; try congruence; eauto.
  now move⇒ [<-] //.
Qed.

Lemma atom_mkApps {t l} : atom (mkApps t l) atom t l = [].
Proof.
  induction l in t |- *; simpl; auto.
  intros. destruct (IHl _ H). discriminate.
Qed.

Lemma pred_atom_mkApps {t l} : pred_atom (mkApps t l) pred_atom t l = [].
Proof.
  induction l in t |- *; simpl; auto.
  intros. destruct (IHl _ H). discriminate.
Qed.

Ltac finish_discr :=
  repeat PCUICAstUtils.finish_discr ||
         match goal with
         | [ H : atom (mkApps _ _) |- _ ] ⇒ apply atom_mkApps in H; intuition subst
         | [ H : pred_atom (mkApps _ _) |- _ ] ⇒ apply pred_atom_mkApps in H; intuition subst
         end.

Ltac solve_discr ::=
  (try (progress (prepare_discr; finish_discr; cbn [mkApps] in × )));
  (try (match goal with
        | [ H : is_true (atom _) |- _ ] ⇒ discriminate
        | [ H : is_true (atom (mkApps _ _)) |- _ ] ⇒ destruct (atom_mkApps H); subst; try discriminate
        | [ H : is_true (pred_atom _) |- _ ] ⇒ discriminate
        | [ H : is_true (pred_atom (mkApps _ _)) |- _ ] ⇒ destruct (pred_atom_mkApps H); subst; try discriminate
        end)).

Section Pred1_inversion.

  Lemma pred_snd_nth:
     (Σ : global_env) (Γ Δ : context) (c : nat) (brs1 brs' : list (nat × term)),
      All2
        (on_Trel (pred1 Σ Γ Δ) snd) brs1
        brs'
        pred1_ctx Σ Γ Δ
      pred1 Σ Γ Δ
              (snd (nth c brs1 (0, tDummy)))
              (snd (nth c brs' (0, tDummy))).
  Proof.
    intros Σ Γ Δ c brs1 brs' brsl. intros.
    induction brsl in c |- *; simpl. destruct c; now apply pred1_refl_gen.
    destruct c; auto.
  Qed.

  Lemma pred_mkApps Σ Γ Δ M0 M1 N0 N1 :
    pred1 Σ Γ Δ M0 M1
    All2 (pred1 Σ Γ Δ) N0 N1
    pred1 Σ Γ Δ (mkApps M0 N0) (mkApps M1 N1).
  Proof.
    intros.
    induction X0 in M0, M1, X |- ×. auto.
    simpl. eapply IHX0. now eapply pred_app.
  Qed.

  Lemma pred1_mkApps_tConstruct (Σ : global_env) (Γ Δ : context)
        ind pars k (args : list term) c :
    pred1 Σ Γ Δ (mkApps (tConstruct ind pars k) args) c
    {args' : list term & (c = mkApps (tConstruct ind pars k) args') × (All2 (pred1 Σ Γ Δ) args args') }%type.
  Proof with solve_discr.
    revert c. induction args using rev_ind; intros; simpl in ×.
    depelim X... []. intuition auto.
    intros. rewrite mkApps_app in X.
    depelim X...
    prepare_discr. apply mkApps_eq_decompose_app in H.
    rewrite !decompose_app_rec_mkApps in H. noconf H.
    destruct (IHargs _ X1) as [args' [-> Hargs']].
     (args' ++ [N1]).
    rewrite mkApps_app. intuition auto.
    eapply All2_app; auto.
  Qed.

  Lemma pred1_mkApps_refl_tConstruct (Σ : global_env) Γ Δ i k u l l' :
    pred1 Σ Γ Δ (mkApps (tConstruct i k u) l) (mkApps (tConstruct i k u) l')
    All2 (pred1 Σ Γ Δ) l l'.
  Proof.
    intros.
    eapply pred1_mkApps_tConstruct in X. destruct X.
    destruct p. now eapply mkApps_eq_inj in e as [_ <-].
  Qed.

  Lemma pred1_mkApps_tInd (Σ : global_env) (Γ Δ : context)
        ind u (args : list term) c :
    pred1 Σ Γ Δ (mkApps (tInd ind u) args) c
    {args' : list term & (c = mkApps (tInd ind u) args') × (All2 (pred1 Σ Γ Δ) args args') }%type.
  Proof with solve_discr.
    revert c. induction args using rev_ind; intros; simpl in ×.
    depelim X... []. intuition auto.
    intros. rewrite mkApps_app in X.
    depelim X... simpl in H; noconf H. solve_discr.
    prepare_discr. apply mkApps_eq_decompose_app in H.
    rewrite !decompose_app_rec_mkApps in H. noconf H.
    destruct (IHargs _ X1) as [args' [-> Hargs']].
     (args' ++ [N1]).
    rewrite mkApps_app. intuition auto.
    eapply All2_app; auto.
  Qed.

  Derive NoConfusion for PCUICEnvironment.global_decl.
  Lemma pred1_mkApps_tRel (Σ : global_env) (Γ Δ : context) k b (args : list term) c :
    nth_error Γ k = Some b decl_body b = None
    pred1 Σ Γ Δ (mkApps (tRel k) args) c
    {args' : list term & (c = mkApps (tRel k) args') × (All2 (pred1 Σ Γ Δ) args args') }%type.
  Proof with solve_discr.
    revert c. induction args using rev_ind; intros; simpl in ×.
    - depelim X...
      × []. intuition auto.
        eapply nth_error_pred1_ctx in a; eauto.
        destruct a as [body' [eqopt _]]. rewrite H /= H0 in eqopt. discriminate.
      × []; intuition auto.
    - rewrite mkApps_app /= in X.
      depelim X; try (simpl in H1; noconf H1); solve_discr.
      × prepare_discr. apply mkApps_eq_decompose_app in H1.
        rewrite !decompose_app_rec_mkApps in H1. noconf H1.
      × destruct (IHargs _ H H0 X1) as [args' [-> Hargs']].
         (args' ++ [N1]).
        rewrite mkApps_app. intuition auto.
        eapply All2_app; auto.
  Qed.

  Lemma pred1_mkApps_tConst_axiom (Σ : global_env) (Γ Δ : context)
        cst u (args : list term) cb c :
    declared_constant Σ cst cb cst_body cb = None
    pred1 Σ Γ Δ (mkApps (tConst cst u) args) c
    {args' : list term & (c = mkApps (tConst cst u) args') × (All2 (pred1 Σ Γ Δ) args args') }%type.
  Proof with solve_discr.
    revert c. induction args using rev_ind; intros; simpl in ×.
    depelim X...
    - red in H, isdecl. rewrite isdecl in H; noconf H.
      congruence.
    - []. intuition auto.
    - rewrite mkApps_app in X.
      depelim X...
      × prepare_discr. apply mkApps_eq_decompose_app in H1.
        rewrite !decompose_app_rec_mkApps in H1. noconf H1.
      × destruct (IHargs _ H H0 X1) as [args' [-> Hargs']].
         (args' ++ [N1]).
        rewrite mkApps_app. intuition auto.
        eapply All2_app; auto.
  Qed.

  Lemma pred1_mkApps_tFix_inv Σ (Γ Δ : context)
        mfix0 idx (args0 : list term) c d :
    nth_error mfix0 idx = Some d
    ~~ is_constructor (rarg d) args0
    pred1 Σ Γ Δ (mkApps (tFix mfix0 idx) args0) c
    ({ mfix1 & { args1 : list term &
                         (c = mkApps (tFix mfix1 idx) args1) ×
                         All2_prop2_eq Γ Δ (Γ ,,, fix_context mfix0) (Δ ,,, fix_context mfix1)
                                       dtype dbody
                                    (fun x(dname x, rarg x))
                                    (pred1 Σ) mfix0 mfix1 ×
                         (All2 (pred1 Σ Γ Δ) ) args0 args1 } }%type).
  Proof with solve_discr.
    intros hnth isc pred. remember (mkApps _ _) as fixt.
    revert mfix0 idx args0 Heqfixt hnth isc.
    induction pred; intros; solve_discr.
    - unfold unfold_fix in e.
      red in a1.
      eapply All2_nth_error_Some in a1; eauto.
      destruct a1 as [t' [ht' [hds [hr [= eqna eqrarg]]]]].
      rewrite ht' in e ⇒ //. noconf e. rewrite -eqrarg in e0.
      rewrite e0 in isc ⇒ //.
    - destruct args0 using rev_ind. noconf Heqfixt. clear IHargs0.
      rewrite mkApps_app in Heqfixt. noconf Heqfixt.
      clear IHpred2. specialize (IHpred1 _ _ _ eq_refl).
      specialize (IHpred1 hnth). apply is_constructor_prefix in isc.
      specialize (IHpred1 isc).
      destruct IHpred1 as [? [? [[? ?] ?]]].
      eexists _. eexists (_ ++ [N1]). rewrite mkApps_app.
      intuition eauto. simpl. subst M1. reflexivity.
      eapply All2_app; eauto.
    - mfix1, []. intuition auto.
    - subst t. solve_discr.
  Qed.

  Lemma pred1_mkApps_tFix_refl_inv (Σ : global_env) (Γ Δ : context)
        mfix0 mfix1 idx0 idx1 (args0 args1 : list term) d :
    nth_error mfix0 idx0 = Some d
    is_constructor (rarg d) args0 = false
    pred1 Σ Γ Δ (mkApps (tFix mfix0 idx0) args0) (mkApps (tFix mfix1 idx1) args1)
    (All2_prop2_eq Γ Δ (Γ ,,, fix_context mfix0) (Δ ,,, fix_context mfix1)
                   dtype dbody
                   (fun x(dname x, rarg x))
                   (pred1 Σ) mfix0 mfix1 ×
     (All2 (pred1 Σ Γ Δ) ) args0 args1).
  Proof with solve_discr.
    intros Hnth Hisc.
    remember (mkApps _ _) as fixt.
    remember (mkApps _ args1) as fixt'.
    intros pred. revert mfix0 mfix1 idx0 args0 d Hnth Hisc idx1 args1 Heqfixt Heqfixt'.
    induction pred; intros; solve_discr.
    -
      red in a1. eapply All2_nth_error_Some in a1; eauto.
      destruct a1 as [t' [Hnth' [Hty [Hpred Hann]]]].
      unfold unfold_fix in e. destruct (nth_error mfix1 idx) eqn:hfix1.
      noconf e. noconf Hnth'.
      move: Hann ⇒ [=] Hname Hrarg.
      all:congruence.

    - destruct args0 using rev_ind; noconf Heqfixt. clear IHargs0.
      rewrite mkApps_app in Heqfixt. noconf Heqfixt.
      destruct args1 using rev_ind; noconf Heqfixt'. clear IHargs1.
      rewrite mkApps_app in Heqfixt'. noconf Heqfixt'.
      clear IHpred2.
      assert (is_constructor (rarg d) args0 = false).
      { move: Hisc. rewrite /is_constructor.
        elim: nth_error_spec. rewrite app_length.
        movei hi harg. elim: nth_error_spec.
        movei' hi' hrarg'.
        rewrite nth_error_app_lt in hi; eauto. congruence.
        auto.
        rewrite app_length. movege _.
        elim: nth_error_spec; intros; try lia; auto.
      }
      specialize (IHpred1 _ _ _ _ _ Hnth H _ _ eq_refl eq_refl).
      destruct IHpred1 as [? ?]. red in a.
      unfold All2_prop2_eq. split. apply a. apply All2_app; auto.
    - constructor; auto.
    - subst. solve_discr.
  Qed.

  Lemma pred1_mkApps_tCoFix_inv (Σ : global_env) (Γ Δ : context)
        mfix0 idx (args0 : list term) c :
    pred1 Σ Γ Δ (mkApps (tCoFix mfix0 idx) args0) c
     mfix1 args1,
      (c = mkApps (tCoFix mfix1 idx) args1) ×
      All2_prop2_eq Γ Δ (Γ ,,, fix_context mfix0) (Δ ,,, fix_context mfix1) dtype dbody
                    (fun x(dname x, rarg x))
                    (pred1 Σ) mfix0 mfix1 ×
      (All2 (pred1 Σ Γ Δ) ) args0 args1.
  Proof with solve_discr.
    intros pred. remember (mkApps _ _) as fixt. revert mfix0 idx args0 Heqfixt.
    induction pred; intros; solve_discr.
    - destruct args0 using rev_ind. noconf Heqfixt. clear IHargs0.
      rewrite mkApps_app in Heqfixt. noconf Heqfixt.
      clear IHpred2. specialize (IHpred1 _ _ _ eq_refl).
      destruct IHpred1 as [? [? [[-> ?] ?]]].
      eexists x, (x0 ++ [N1]). intuition auto.
      now rewrite mkApps_app.
      eapply All2_app; eauto.
    - mfix1, []; intuition (simpl; auto).
    - subst t; solve_discr.
  Qed.

  Lemma pred1_mkApps_tCoFix_refl_inv (Σ : global_env) (Γ Δ : context)
        mfix0 mfix1 idx (args0 args1 : list term) :
    pred1 Σ Γ Δ (mkApps (tCoFix mfix0 idx) args0) (mkApps (tCoFix mfix1 idx) args1)
      All2_prop2_eq Γ Δ (Γ ,,, fix_context mfix0) (Δ ,,, fix_context mfix1) dtype dbody
                    (fun x(dname x, rarg x))
                    (pred1 Σ) mfix0 mfix1 ×
      (All2 (pred1 Σ Γ Δ)) args0 args1.
  Proof with solve_discr.
    intros pred. remember (mkApps _ _) as fixt.
    remember (mkApps _ args1) as fixt'.
    revert mfix0 mfix1 idx args0 args1 Heqfixt Heqfixt'.
    induction pred; intros; symmetry in Heqfixt; solve_discr.
    - destruct args0 using rev_ind. noconf Heqfixt. clear IHargs0.
      rewrite mkApps_app in Heqfixt. noconf Heqfixt.
      clear IHpred2.
      symmetry in Heqfixt'.
      destruct args1 using rev_ind. discriminate. rewrite mkApps_app in Heqfixt'.
      noconf Heqfixt'.
      destruct (IHpred1 _ _ _ _ _ eq_refl eq_refl) as [H H'].
      unfold All2_prop2_eq. split. apply H. apply All2_app; auto.
    - repeat finish_discr.
      unfold All2_prop2_eq. intuition (simpl; auto).
    - subst t; solve_discr.
  Qed.

End Pred1_inversion.

#[global]
Hint Constructors pred1 : pcuic.

Notation predicate_depth := (predicate_depth_gen depth).
Notation fold_context_term f := (fold_context (fun Γ'map_decl (f Γ'))).

Section Rho.
  Context {cf : checker_flags}.
  Context (Σ : global_env).
  Context (wfΣ : wf Σ).

  #[program] Definition map_fix_rho {t} (rho : context x, depth x < depth t term) Γ mfixctx (mfix : mfixpoint term)
    (H : mfixpoint_depth mfix < depth t) :=
    (map_In mfix (fun d (H : In d mfix) ⇒ {| dname := dname d;
        dtype := rho Γ (dtype d) _;
        dbody := rho (Γ ,,, mfixctx) (dbody d) _; rarg := (rarg d) |})).
  Next Obligation.
    eapply (In_list_depth (def_depth_gen depth)) in H.
    eapply Nat.le_lt_trans with (def_depth_gen depth d).
    unfold def_depth_gen. lia.
    unfold mfixpoint_depth in H0.
    lia.
  Qed.
  Next Obligation.
    eapply (In_list_depth (def_depth_gen depth)) in H.
    eapply Nat.le_lt_trans with (def_depth_gen depth d).
    unfold def_depth_gen. lia.
    unfold mfixpoint_depth in H0.
    lia.
  Qed.

  Equations? fold_fix_context_wf mfix
      (rho : context x, depth x (mfixpoint_depth mfix) term)
      (Γ acc : context) : context :=
  fold_fix_context_wf [] rho Γ accacc ;
  fold_fix_context_wf (d :: mfix) rho Γ acc
    fold_fix_context_wf mfix (fun Γ x Hxrho Γ x _) Γ (vass (dname d) (lift0 #|acc| (rho Γ (dtype d) _)) :: acc).
  Proof.
    lia. unfold def_depth_gen. lia.
  Qed.
  Transparent fold_fix_context_wf.

  #[program] Definition map_terms {t} (rho : context x, depth x < depth t term) Γ (l : list term)
    (H : list_depth_gen depth l < depth t) :=
    (map_In l (fun t (H : In t l) ⇒ rho Γ t _)).
  Next Obligation.
    eapply (In_list_depth depth) in H. lia.
  Qed.

  Section rho_ctx.
    Context (Γ : context).
    Context (rho : context x, depth x context_depth Γ term).

    Program Definition rho_ctx_over_wf :=
      fold_context_In Γ (fun Γ' d hin
        match d with
        | {| decl_name := na; decl_body := None; decl_type := T |} ⇒
            vass na (rho Γ' T _)
        | {| decl_name := na; decl_body := Some b; decl_type := T |} ⇒
          vdef na (rho Γ' b _) (rho Γ' T _)
        end).

      Next Obligation.
        eapply (In_list_depth (decl_depth_gen depth)) in hin.
        unfold decl_depth_gen at 1 in hin. simpl in ×. unfold context_depth. lia.
      Qed.
      Next Obligation.
        eapply (In_list_depth (decl_depth_gen depth)) in hin.
        unfold decl_depth_gen at 1 in hin. simpl in ×. unfold context_depth. lia.
      Qed.
      Next Obligation.
        eapply (In_list_depth (decl_depth_gen depth)) in hin.
        unfold decl_depth_gen at 1 in hin. simpl in ×. unfold context_depth. lia.
      Qed.
  End rho_ctx.

  Lemma rho_ctx_over_wf_eq (rho : context term term) (Γ : context) :
    rho_ctx_over_wf Γ (fun Γ x hinrho Γ x) =
    fold_context_term rho Γ.
  Proof using Type.
    rewrite /rho_ctx_over_wf fold_context_In_spec.
    apply fold_context_Proper. intros n x.
    now destruct x as [na [b|] ty]; simpl.
  Qed.
  Hint Rewrite rho_ctx_over_wf_eq : rho.

  #[program]
  Definition map_br_wf {t} (rho : context x, depth x < depth t term)
    Γ (p : PCUICAst.predicate term)
    (br : branch term) (H : depth (bbody br) < depth t) :=
    let bcontext' := inst_case_branch_context p br in
    {| bcontext := br.(bcontext);
       bbody := rho (Γ ,,, bcontext') br.(bbody) _ |}.

  Definition map_br_gen (rho : context term term) Γ p (br : branch term) :=
    let bcontext' := inst_case_branch_context p br in
    {| bcontext := br.(bcontext);
       bbody := rho (Γ ,,, bcontext') br.(bbody) |}.

  Lemma map_br_map (rho : context term term) t Γ p l H :
    @map_br_wf t (fun Γ x Hxrho Γ x) Γ p l H = map_br_gen rho Γ p l.
  Proof using Type.
    unfold map_br_wf, map_br_gen. now f_equal; autorewrite with rho.
  Qed.
  Hint Rewrite map_br_map : rho.

  #[program] Definition map_brs_wf {t} (rho : context x, depth x < depth t term) Γ
    p (l : list (branch term))
    (H : list_depth_gen (depth bbody) l < depth t) :=
    map_In l (fun br (H : In br l) ⇒ map_br_wf rho Γ p br _).
  Next Obligation.
    eapply (In_list_depth (depth bbody)) in H. lia.
  Qed.

  Lemma map_brs_map (rho : context term term) t Γ p l H :
    @map_brs_wf t (fun Γ x Hxrho Γ x) Γ p l H = map (map_br_gen rho Γ p) l.
  Proof using Type.
    unfold map_brs_wf, map_br_wf. rewrite map_In_spec.
    apply map_extx. now autorewrite with rho.
  Qed.
  Hint Rewrite map_brs_map : rho.

  #[program] Definition rho_predicate_wf {t} (rho : context x, depth x < depth t term) Γ
    (p : PCUICAst.predicate term) (H : predicate_depth p < depth t) :=
    let params' := map_terms rho Γ p.(pparams) _ in
    let pcontext' := inst_case_context params' p.(puinst) p.(pcontext) in
    {| pparams := params';
     puinst := p.(puinst) ;
     pcontext := p.(pcontext) ;
     preturn := rho (Γ ,,, pcontext') p.(preturn) _ |}.
    Next Obligation.
      pose proof (context_depth_inst_case_context p.(pparams) p.(puinst) p.(pcontext)).
      rewrite /predicate_depth in H. lia.
    Qed.
    Next Obligation.
      rewrite /predicate_depth in H. lia.
    Qed.

  Definition rho_predicate_gen (rho : context term term) Γ
    (p : PCUICAst.predicate term) :=
    let params' := map (rho Γ) p.(pparams) in
    let pcontext' := inst_case_context params' p.(puinst) p.(pcontext) in
    {| pparams := params';
       puinst := p.(puinst) ;
       pcontext := p.(pcontext) ;
       preturn := rho (Γ ,,, pcontext') p.(preturn) |}.

  Lemma map_terms_map (rho : context term term) t Γ l H :
    @map_terms t (fun Γ x Hxrho Γ x) Γ l H = map (rho Γ) l.
  Proof using Type.
    unfold map_terms. now rewrite map_In_spec.
  Qed.
  Hint Rewrite map_terms_map : rho.

  Lemma rho_predicate_map_predicate {t} (rho : context term term) Γ p (H : predicate_depth p < depth t) :
    rho_predicate_wf (fun Γ x Hrho Γ x) Γ p H =
    rho_predicate_gen rho Γ p.
  Proof using Type.
    rewrite /rho_predicate_gen /rho_predicate_wf.
    f_equal; simp rho ⇒ //.
  Qed.
  Hint Rewrite @rho_predicate_map_predicate : rho.

  Definition inspect {A} (x : A) : { y : A | x = y } := exist x eq_refl.

  Arguments Nat.max : simpl never.

  #[program]
  Definition rho_iota_red_wf {t} (rho : context x, depth x < depth t term) Γ
    (p : PCUICAst.predicate term) npar (args : list term) (br : branch term)
    (H : depth (bbody br) < depth t) :=
    let bctx := inst_case_branch_context p br in
    
    let br' := map_br_wf rho Γ p br _ in
    subst0 (List.rev (skipn npar args)) (expand_lets bctx (bbody br')).

  Definition rho_iota_red_gen (rho : context term term) Γ
    (p : PCUICAst.predicate term) npar (args : list term) (br : branch term) :=
    let bctx := inst_case_branch_context p br in
    
    subst0 (List.rev (skipn npar args)) (expand_lets bctx (rho (Γ ,,, bctx) (bbody br))).

  Lemma rho_iota_red_wf_gen (rho : context term term) t Γ p npar args br H :
    rho_iota_red_wf (t:=t) (fun Γ x Hrho Γ x) Γ p npar args br H =
    rho_iota_red_gen rho Γ p npar args br.
  Proof using Type.
    rewrite /rho_iota_red_wf /rho_iota_red_gen. f_equal.
  Qed.
  Hint Rewrite @rho_iota_red_wf_gen : rho.

  Lemma bbody_branch_depth brs p :
    list_depth_gen (depth bbody) brs <
    S (list_depth_gen (branch_depth_gen depth p) brs).
  Proof using Type.
    rewrite /branch_depth_gen.
    induction brs; simpl; auto. lia.
  Qed.

Needs well-founded recursion on the depth of terms as we should reduce strings of applications in one go.
  Equations? rho (Γ : context) (t : term) : term by wf (depth t) :=
  rho Γ (tApp t u) with view_lambda_fix_app t u :=
    { | fix_lambda_app_lambda na T b [] u :=
        (rho (vass na (rho Γ T) :: Γ) b) {0 := rho Γ u};
      | fix_lambda_app_lambda na T b (a :: l) u :=
        mkApps ((rho (vass na (rho Γ T) :: Γ) b) {0 := rho Γ a})
          (map_terms rho Γ (l ++ [u]) _);
      | fix_lambda_app_fix mfix idx l u :=
        let mfixctx := fold_fix_context_wf mfix (fun Γ x Hxrho Γ x) Γ [] in
        let mfix' := map_fix_rho (t:=tFix mfix idx) (fun Γ x Hxrho Γ x) Γ mfixctx mfix _ in
        let args := map_terms rho Γ (l ++ [u]) _ in
        match unfold_fix mfix' idx with
        | Some (rarg, fn)
          if is_constructor rarg (l ++ [u]) then
            mkApps fn args
          else mkApps (tFix mfix' idx) args
        | NonemkApps (tFix mfix' idx) args
        end ;
      | fix_lambda_app_other t u nisfixlam := tApp (rho Γ t) (rho Γ u) } ;
  rho Γ (tLetIn na d t b) ⇒ (subst10 (rho Γ d) (rho (vdef na (rho Γ d) (rho Γ t) :: Γ) b));
  rho Γ (tRel i) with option_map decl_body (nth_error Γ i) := {
    | Some (Some body) ⇒ (lift0 (S i) body);
    | Some NonetRel i;
    | NonetRel i };

  rho Γ (tCase ci p x brs) with inspect (decompose_app x) :=
  { | exist (f, args) eqx with view_construct_cofix f :=
  { | construct_cofix_construct ind' c u with eq_inductive ci.(ci_ind) ind' :=
    { | true with inspect (nth_error brs c) ⇒
        { | exist (Some br) eqbr
            if eqb #|args|
              (ci_npar ci + context_assumptions (bcontext br)) then
              let p' := rho_predicate_wf rho Γ p _ in
              let args' := map_terms rho Γ args _ in
              rho_iota_red_wf rho Γ p' ci.(ci_npar) args' br _
            else
              let p' := rho_predicate_wf rho Γ p _ in
              let brs' := map_brs_wf rho Γ p' brs _ in
              let x' := rho Γ x in
              tCase ci p' x' brs';
          | exist None eqbr
            let p' := rho_predicate_wf rho Γ p _ in
            let brs' := map_brs_wf rho Γ p' brs _ in
            let x' := rho Γ x in
            tCase ci p' x' brs' };
      | false
        let p' := rho_predicate_wf rho Γ p _ in
        let x' := rho Γ x in
        let brs' := map_brs_wf rho Γ p' brs _ in
        tCase ci p' x' brs' };
    | construct_cofix_cofix mfix idx :=
      let p' := rho_predicate_wf rho Γ p _ in
      let args' := map_terms rho Γ args _ in
      let brs' := map_brs_wf rho Γ p' brs _ in
      let mfixctx := fold_fix_context_wf mfix (fun Γ x Hxrho Γ x) Γ [] in
      let mfix' := map_fix_rho (t:=tCase ci p x brs) rho Γ mfixctx mfix _ in
        match nth_error mfix' idx with
        | Some d
          tCase ci p' (mkApps (subst0 (cofix_subst mfix') (dbody d)) args') brs'
        | NonetCase ci p' (rho Γ x) brs'
        end;
    | construct_cofix_other _ nconscof
      let p' := rho_predicate_wf rho Γ p _ in
      let x' := rho Γ x in
      let brs' := map_brs_wf rho Γ p' brs _ in
        tCase ci p' x' brs' } };

  rho Γ (tProj p x) with inspect (decompose_app x) := {
    | exist (f, args) eqx with view_construct0_cofix f :=
    | construct0_cofix_construct ind u with
        inspect (nth_error (map_terms rho Γ args _) (p.(proj_npars) + p.(proj_arg))) := {
      | exist (Some arg1) eq
        if eq_inductive p.(proj_ind) ind then arg1
        else tProj p (rho Γ x);
      | exist None neqtProj p (rho Γ x) };
    | construct0_cofix_cofix mfix idx :=
      let args' := map_terms rho Γ args _ in
      let mfixctx := fold_fix_context_wf mfix (fun Γ x Hxrho Γ x) Γ [] in
      let mfix' := map_fix_rho (t:=tProj p x) rho Γ mfixctx mfix _ in
      match nth_error mfix' idx with
      | Some dtProj p (mkApps (subst0 (cofix_subst mfix') (dbody d)) args')
      | NonetProj p (rho Γ x)
      end;
    | construct0_cofix_other f nconscoftProj p (rho Γ x) } ;
  rho Γ (tConst c u) with lookup_env Σ c := {
    | Some (ConstantDecl decl) with decl.(cst_body) := {
      | Some bodysubst_instance u body;
      | NonetConst c u };
    | _tConst c u };
  rho Γ (tLambda na t u) ⇒ tLambda na (rho Γ t) (rho (vass na (rho Γ t) :: Γ) u);
  rho Γ (tProd na t u) ⇒ tProd na (rho Γ t) (rho (vass na (rho Γ t) :: Γ) u);
  rho Γ (tVar i) ⇒ tVar i;
  rho Γ (tEvar n l) ⇒ tEvar n (map_terms rho Γ l _);
  rho Γ (tSort s) ⇒ tSort s;
  rho Γ (tFix mfix idx) ⇒
    let mfixctx := fold_fix_context_wf mfix (fun Γ x Hxrho Γ x) Γ [] in
    tFix (map_fix_rho (t:=tFix mfix idx) (fun Γ x Hxrho Γ x) Γ mfixctx mfix _) idx;
  rho Γ (tCoFix mfix idx) ⇒
    let mfixctx := fold_fix_context_wf mfix (fun Γ x Hxrho Γ x) Γ [] in
    tCoFix (map_fix_rho (t:=tCoFix mfix idx) rho Γ mfixctx mfix _) idx;
  rho Γ xx.
  Proof.
    all:try abstract lia.
    Ltac d :=
      match goal with
      |- context [depth (mkApps ?f ?l)] ⇒
        move: (depth_mkApps f l); cbn -[Nat.max]; try lia
      end.
    Ltac invd :=
      match goal with
      [ H : decompose_app ?x = _ |- _ ] ⇒
        eapply decompose_app_inv in H; subst x
      end.
    all:try abstract (rewrite ?list_depth_app; d).
    all:try solve [clear -eqx; abstract (invd; d)].
    all:try solve [clear; move:(bbody_branch_depth brs p); lia].
    - clear -eqbr.
      abstract (eapply (nth_error_depth (branch_depth_gen depth p)) in eqbr;
      unfold branch_depth_gen in eqbr |- *; lia).
    - clear -eqx Hx. abstract (invd; d).
    - clear -eqx Hx. abstract (invd; d).
  Defined.

  Notation rho_predicate := (rho_predicate_gen rho).
  Notation rho_br := (map_br_gen rho).
  Notation rho_ctx_over Γ :=
    (fold_context (fun Δmap_decl (rho (Γ ,,, Δ)))).
  Notation rho_ctx := (fold_context_term rho).
  Notation rho_iota_red := (rho_iota_red_gen rho).

  Lemma rho_ctx_over_length Δ Γ : #|rho_ctx_over Δ Γ| = #|Γ|.
  Proof using Type.
    now rewrite fold_context_length.
  Qed.

  Definition rho_fix_context Γ mfix :=
    fold_fix_context rho Γ [] mfix.

  Lemma rho_fix_context_length Γ mfix : #|rho_fix_context Γ mfix| = #|mfix|.
  Proof using Type. now rewrite fold_fix_context_length Nat.add_0_r. Qed.



  Definition map_fix (rho : context term term) Γ mfixctx (mfix : mfixpoint term) :=
    (map (map_def (rho Γ) (rho (Γ ,,, mfixctx))) mfix).

  Lemma map_fix_rho_map t Γ mfix ctx H :
    @map_fix_rho t (fun Γ x Hxrho Γ x) Γ ctx mfix H =
    map_fix rho Γ ctx mfix.
  Proof using Type.
    unfold map_fix_rho. now rewrite map_In_spec.
  Qed.

  Lemma fold_fix_context_wf_fold mfix Γ ctx :
    fold_fix_context_wf mfix (fun Γ x _rho Γ x) Γ ctx =
    fold_fix_context rho Γ ctx mfix.
  Proof using Type.
    induction mfix in ctx |- *; simpl; auto.
  Qed.

  Hint Rewrite map_fix_rho_map fold_fix_context_wf_fold : rho.

  Ltac discr_mkApps H :=
    let Hf := fresh in let Hargs := fresh in
    rewrite ?tApp_mkApps -?mkApps_app in H;
      (eapply mkApps_nApp_inj in H as [Hf Hargs] ||
        eapply (mkApps_nApp_inj _ _ []) in H as [Hf Hargs] ||
        eapply (mkApps_nApp_inj _ _ _ []) in H as [Hf Hargs]);
        [noconf Hf|reflexivity].

  Set Equations With UIP.
  Lemma rho_app_lambda Γ na ty b a l :
    rho Γ (mkApps (tApp (tLambda na ty b) a) l) =
    mkApps ((rho (vass na (rho Γ ty) :: Γ) b) {0 := rho Γ a}) (map (rho Γ) l).
  Proof using Type.
    induction l using rev_ind; autorewrite with rho.
    - simpl. reflexivity.
    - simpl. rewrite mkApps_app. autorewrite with rho.
      change (mkApps (tApp (tLambda na ty b) a) l) with
        (mkApps (tLambda na ty b) (a :: l)).
      now simp rho.
  Qed.

  Lemma rho_app_lambda' Γ na ty b l :
    rho Γ (mkApps (tLambda na ty b) l) =
    match l with
    | []rho Γ (tLambda na ty b)
    | a :: l
      mkApps ((rho (vass na (rho Γ ty) :: Γ) b) {0 := rho Γ a}) (map (rho Γ) l)
    end.
  Proof using Type.
    destruct l using rev_case; autorewrite with rho; auto.
    simpl. rewrite mkApps_app. simp rho.
    destruct l; simpl; auto. now simp rho.
  Qed.

  Lemma rho_app_construct Γ c u i l :
    rho Γ (mkApps (tConstruct c u i) l) =
    mkApps (tConstruct c u i) (map (rho Γ) l).
  Proof using Type.
    induction l using rev_ind; autorewrite with rho; auto.
    simpl. rewrite mkApps_app. simp rho.
    unshelve erewrite view_lambda_fix_app_other. simpl.
    clear; induction l using rev_ind; simpl; auto.
    rewrite mkApps_app. simpl. apply IHl.
    simp rho. rewrite IHl. now rewrite map_app mkApps_app.
  Qed.
  Hint Rewrite rho_app_construct : rho.

  Lemma rho_app_cofix Γ mfix idx l :
    rho Γ (mkApps (tCoFix mfix idx) l) =
    mkApps (tCoFix (map_fix rho Γ (rho_fix_context Γ mfix) mfix) idx) (map (rho Γ) l).
  Proof using Type.
    induction l using rev_ind; autorewrite with rho; auto.
    simpl. now simp rho. rewrite mkApps_app. simp rho.
    unshelve erewrite view_lambda_fix_app_other. simpl.
    clear; induction l using rev_ind; simpl; auto.
    rewrite mkApps_app. simpl. apply IHl.
    simp rho. rewrite IHl. now rewrite map_app mkApps_app.
  Qed.

  Hint Rewrite rho_app_cofix : rho.

  Lemma map_cofix_subst (f : context term term)
        (f' : context context term term) mfix Γ Γ' :
    ( n, tCoFix (map (map_def (f Γ) (f' Γ Γ')) mfix) n = f Γ (tCoFix mfix n))
    cofix_subst (map (map_def (f Γ) (f' Γ Γ')) mfix) =
    map (f Γ) (cofix_subst mfix).
  Proof using Type.
    unfold cofix_subst. intros.
    rewrite map_length. generalize (#|mfix|). induction n. simpl. reflexivity.
    simpl. rewrite - IHn. f_equal. apply H.
  Qed.

  Lemma map_cofix_subst' f g mfix :
    ( n, tCoFix (map (map_def f g) mfix) n = f (tCoFix mfix n))
    cofix_subst (map (map_def f g) mfix) =
    map f (cofix_subst mfix).
  Proof using Type.
    unfold cofix_subst. intros.
    rewrite map_length. generalize (#|mfix|) at 1 2. induction n. simpl. reflexivity.
    simpl. rewrite - IHn. f_equal. apply H.
  Qed.

  Lemma map_fix_subst f g mfix :
    ( n, tFix (map (map_def f g) mfix) n = f (tFix mfix n))
    fix_subst (map (map_def f g) mfix) =
    map f (fix_subst mfix).
  Proof using Type.
    unfold fix_subst. intros.
    rewrite map_length. generalize (#|mfix|) at 1 2. induction n. simpl. reflexivity.
    simpl. rewrite - IHn. f_equal. apply H.
  Qed.

  Lemma rho_app_fix Γ mfix idx args :
    let rhoargs := map (rho Γ) args in
    rho Γ (mkApps (tFix mfix idx) args) =
      match nth_error mfix idx with
      | Some d
        if is_constructor (rarg d) args then
          let fn := (subst0 (map (rho Γ) (fix_subst mfix))) (rho (Γ ,,, fold_fix_context rho Γ [] mfix) (dbody d)) in
          mkApps fn rhoargs
        else mkApps (rho Γ (tFix mfix idx)) rhoargs
      | NonemkApps (rho Γ (tFix mfix idx)) rhoargs
      end.
  Proof using Type.
    induction args using rev_ind; autorewrite with rho.
    - intros rhoargs.
      destruct nth_error as [d|] eqn:eqfix ⇒ //.
      rewrite /is_constructor nth_error_nil //.
    - simpl. rewrite map_app /=.
      destruct nth_error as [d|] eqn:eqfix ⇒ //.
      destruct (is_constructor (rarg d) (args ++ [x])) eqn:isc; simp rho.
      × rewrite mkApps_app /=.
        autorewrite with rho.
        simpl. simp rho. rewrite /unfold_fix.
        rewrite /map_fix nth_error_map eqfix /= isc map_fix_subst ?map_app //.
        intros n; simp rho. simpl. f_equal; now simp rho.
      × rewrite mkApps_app /=.
        simp rho. simpl. simp rho.
        now rewrite /unfold_fix /map_fix nth_error_map eqfix /= isc map_app.
      × rewrite mkApps_app /=. simp rho.
        simpl. simp rho.
        now rewrite /unfold_fix /map_fix nth_error_map eqfix /= map_app.
  Qed.

  Inductive rho_fix_spec Γ mfix i l : term Type :=
  | rho_fix_red d :
      let fn := (subst0 (map (rho Γ) (fix_subst mfix))) (rho (Γ ,,, rho_fix_context Γ mfix) (dbody d)) in
      nth_error mfix i = Some d
      is_constructor (rarg d) l
      rho_fix_spec Γ mfix i l (mkApps fn (map (rho Γ) l))
  | rho_fix_stuck :
      (match nth_error mfix i with
       | Nonetrue
       | Some d~~ is_constructor (rarg d) l
       end)
      rho_fix_spec Γ mfix i l (mkApps (rho Γ (tFix mfix i)) (map (rho Γ) l)).

  Lemma rho_fix_elim Γ mfix i l :
    rho_fix_spec Γ mfix i l (rho Γ (mkApps (tFix mfix i) l)).
  Proof using Type.
    rewrite rho_app_fix /= /unfold_fix.
    case e: nth_error ⇒ [d|] /=.
    case isc: is_constructor ⇒ /=.
    - eapply (rho_fix_red Γ mfix i l d) ⇒ //.
    - apply rho_fix_stuck.
      now rewrite e isc.
    - apply rho_fix_stuck. now rewrite e /=.
  Qed.

  Lemma rho_app_case Γ ci p x brs :
    rho Γ (tCase ci p x brs) =
    let (f, args) := decompose_app x in
    let p' := rho_predicate Γ p in
    match f with
    | tConstruct ind' c u
      if eq_inductive ci.(ci_ind) ind' then
        match nth_error brs c with
        | Some br
          if eqb #|args| (ci_npar ci + context_assumptions (bcontext br)) then
            let args' := map (rho Γ) args in
            rho_iota_red Γ p' ci.(ci_npar) args' br
          else tCase ci p' (rho Γ x) (map (rho_br Γ p') brs)
        | NonetCase ci p' (rho Γ x) (map (rho_br Γ p') brs)
        end
      else tCase ci p' (rho Γ x) (map (rho_br Γ p') brs)
    | tCoFix mfix idx
      match nth_error mfix idx with
      | Some d
        let fn := (subst0 (map (rho Γ) (cofix_subst mfix))) (rho (Γ ,,, fold_fix_context rho Γ [] mfix) (dbody d)) in
        tCase ci (rho_predicate Γ p) (mkApps fn (map (rho Γ) args))
           (map (rho_br Γ p') brs)
      | NonetCase ci p' (rho Γ x) (map (rho_br Γ p') brs)
      end
    | _tCase ci p' (rho Γ x) (map (rho_br Γ p') brs)
    end.
  Proof using Type.
    autorewrite with rho.
    set (app := inspect _).
    destruct app as [[f l] eqapp].
    rewrite {2}eqapp. autorewrite with rho.
    destruct view_construct_cofix; autorewrite with rho.
    destruct eq_inductive eqn:eqi; simp rho ⇒ //.
    destruct inspect as [[br|] eqnth]; cbv zeta; simp rho; rewrite eqnth //; cbv zeta; simp rho ⇒ //.
    simpl; now simp rho.
    cbv zeta.
    simpl. autorewrite with rho. rewrite /map_fix nth_error_map.
    destruct nth_error ⇒ /=. f_equal.
    f_equal. rewrite (map_cofix_subst rho (fun x yrho (x ,,, y))) //.
    intros. autorewrite with rho. simpl. now autorewrite with rho.
    reflexivity.
    simpl.
    autorewrite with rho.
    destruct t; simpl in d ⇒ //.
  Qed.

  Lemma rho_app_proj Γ p x :
    rho Γ (tProj p x) =
    let (f, args) := decompose_app x in
    match f with
    | tConstruct ind' 0 u
      if eq_inductive p.(proj_ind) ind' then
        match nth_error args (p.(proj_npars) + p.(proj_arg)) with
        | Some arg1rho Γ arg1
        | NonetProj p (rho Γ x)
        end
      else tProj p (rho Γ x)
    | tCoFix mfix idx
      match nth_error mfix idx with
      | Some d
        let fn := (subst0 (map (rho Γ) (cofix_subst mfix))) (rho (Γ ,,, fold_fix_context rho Γ [] mfix) (dbody d)) in
        tProj p (mkApps fn (map (rho Γ) args))
      | NonetProj p (rho Γ x)
      end
    | _tProj p (rho Γ x)
    end.
  Proof using Type.
    autorewrite with rho.
    set (app := inspect _).
    destruct app as [[f l] eqapp].
    rewrite {2}eqapp. autorewrite with rho.
    destruct view_construct0_cofix; autorewrite with rho.
    destruct eq_inductive eqn:eqi; simp rho ⇒ //.
    set (arg' := inspect _). clearbody arg'.
    destruct arg' as [[arg'|] eqarg'];
    autorewrite with rho. rewrite eqi.
    simp rho in eqarg'. rewrite nth_error_map in eqarg'.
    destruct nth_error ⇒ //. now simpl in eqarg'.
    simp rho in eqarg'; rewrite nth_error_map in eqarg'.
    destruct nth_error ⇒ //.
    destruct inspect as [[arg'|] eqarg'] ⇒ //; simp rho.
    now rewrite eqi.
    simpl. autorewrite with rho.
    rewrite /map_fix nth_error_map.
    destruct nth_error eqn:nth ⇒ /= //.
    f_equal. f_equal. f_equal.
    rewrite (map_cofix_subst rho (fun x yrho (x ,,, y))) //.
    intros. autorewrite with rho. simpl. now autorewrite with rho.
    simpl. eapply decompose_app_inv in eqapp.
    subst x. destruct t; simpl in d ⇒ //.
    now destruct n.
  Qed.

  Lemma fold_fix_context_rev_mapi {Γ l m} :
    fold_fix_context rho Γ l m =
    List.rev (mapi (fun (i : nat) (x : def term) ⇒
                    vass (dname x) ((lift0 (#|l| + i)) (rho Γ (dtype x)))) m) ++ l.
  Proof using Type.
    unfold mapi.
    rewrite rev_mapi.
    induction m in l |- ×. simpl. auto.
    intros. simpl. rewrite mapi_app. simpl.
    rewrite IHm. cbn.
    rewrite - app_assoc. simpl. rewrite List.rev_length.
    rewrite Nat.add_0_r. rewrite Nat.sub_diag Nat.add_0_r. simpl.
    f_equal. apply mapi_ext_size. simpl; intros.
    rewrite List.rev_length in H. lia_f_equal.
  Qed.

  Lemma fold_fix_context_rev {Γ m} :
    fold_fix_context rho Γ [] m =
    List.rev (mapi (fun (i : nat) (x : def term) ⇒
                    vass (dname x) (lift0 i (rho Γ (dtype x)))) m).
  Proof using Type.
    pose proof (@fold_fix_context_rev_mapi Γ [] m).
    now rewrite app_nil_r in H.
  Qed.

  Lemma nth_error_map_fix i f Γ Δ m :
    nth_error (map_fix f Γ Δ m) i = option_map (map_def (f Γ) (f (Γ ,,, Δ))) (nth_error m i).
  Proof using Type.
    now rewrite /map_fix nth_error_map.
  Qed.

  Lemma fold_fix_context_app Γ l acc acc' :
    fold_fix_context rho Γ l (acc ++ acc') =
    fold_fix_context rho Γ (fold_fix_context rho Γ l acc) acc'.
  Proof using Type.
    induction acc in l, acc' |- ×. simpl. auto.
    simpl. rewrite IHacc. reflexivity.
  Qed.

  Definition pres_bodies Γ Δ σ :=
    All2i_len
     (fun n decl decl' ⇒ (decl_body decl' = option_map (fun xx.[⇑^n σ]) (decl_body decl)))
     Γ Δ.

  Lemma pres_bodies_inst_context Γ σ : pres_bodies Γ (inst_context σ Γ) σ.
  Proof using Type.
    red; induction Γ. constructor.
    rewrite inst_context_snoc. constructor. simpl. reflexivity.
    apply IHΓ.
  Qed.
  Hint Resolve pres_bodies_inst_context : pcuic.

  Definition ctxmap (Γ Δ : context) (s : nat term) :=
     x d, nth_error Γ x = Some d
                match decl_body d return Type with
                | Some b
                   i b', s x = tRel i
                          option_map decl_body (nth_error Δ i) = Some (Some b')
                          b'.[↑^(S i)] = b.[↑^(S x) s s]
                | NoneTrue
                end.

  Lemma All2_prop2_eq_split (Γ Γ' Γ2 Γ2' : context) (A B : Type) (f g : A term)
        (h : A B) (rel : context context term term Type) x y :
    All2_prop2_eq Γ Γ' Γ2 Γ2' f g h rel x y
    All2 (on_Trel (rel Γ Γ') f) x y ×
    All2 (on_Trel (rel Γ2 Γ2') g) x y ×
    All2 (on_Trel eq h) x y.
  Proof using Type.
    induction 1; intuition.
  Qed.

  Lemma refine_pred Γ Δ t u u' : u = u' pred1 Σ Γ Δ t u' pred1 Σ Γ Δ t u.
  Proof using Type. now intros →. Qed.

  Lemma ctxmap_ext Γ Δ : CMorphisms.Proper (CMorphisms.respectful (pointwise_relation _ eq) iffT) (ctxmap Γ Δ).
  Proof using Type.
    red. red. intros.
    split; intros X.
    - intros n d Hn. specialize (X n d Hn).
      destruct d as [na [b|] ty]; simpl in *; auto.
      destruct X as [i [b' [? ?]]]. i, b'.
      rewrite -H. split; auto.
    - intros n d Hn. specialize (X n d Hn).
      destruct d as [na [b|] ty]; simpl in *; auto.
      destruct X as [i [b' [? ?]]]. i, b'.
      rewrite H. split; auto.
  Qed.

  Lemma Up_ctxmap Γ Δ c c' σ :
    ctxmap Γ Δ σ
    (decl_body c' = option_map (fun xx.[σ]) (decl_body c))
    ctxmap (Γ ,, c) (Δ ,, c') ( σ).
  Proof using Type.
    intros.
    intros x d Hnth.
    destruct x; simpl in *; noconf Hnth.
    destruct c as [na [b|] ty]; simpl; auto.
     0. eexists. repeat split; eauto. simpl in H. simpl. now rewrite H.
    now autorewrite with sigma.
    specialize (X _ _ Hnth). destruct decl_body; auto.
    destruct X as [i [b' [? [? ?]]]]; auto.
     (S i), b'. simpl. repeat split; auto.
    unfold subst_compose. now rewrite H0.
    autorewrite with sigma in H2 |- ×.
    rewrite -subst_compose_assoc.
    rewrite -subst_compose_assoc.
    rewrite -subst_compose_assoc.
    rewrite -inst_assoc. rewrite H2.
    now autorewrite with sigma.
  Qed.

  Lemma Upn_ctxmap Γ Δ Γ' Δ' σ :
    pres_bodies Γ' Δ' σ
    ctxmap Γ Δ σ
    ctxmap (Γ ,,, Γ') (Δ ,,, Δ') (⇑^#|Γ'| σ).
  Proof using Type.
    induction 1. simpl. intros.
    eapply ctxmap_ext. rewrite Upn_0. reflexivity. apply X.
    simpl. intros Hσ.
    eapply ctxmap_ext. now sigma.
    eapply Up_ctxmap; eauto.
  Qed.
  Hint Resolve Upn_ctxmap : pcuic.

  Lemma inst_ctxmap Γ Δ Γ' σ :
    ctxmap Γ Δ σ
    ctxmap (Γ ,,, Γ') (Δ ,,, inst_context σ Γ') (⇑^#|Γ'| σ).
  Proof using Type.
    intros cmap.
    apply Upn_ctxmap ⇒ //.
    apply pres_bodies_inst_context.
  Qed.
  Hint Resolve inst_ctxmap : pcuic.

  Lemma inst_ctxmap_up Γ Δ Γ' σ :
    ctxmap Γ Δ σ
    ctxmap (Γ ,,, Γ') (Δ ,,, inst_context σ Γ') (up #|Γ'| σ).
  Proof using Type.
    intros cmap.
    eapply ctxmap_ext. rewrite up_Upn. reflexivity.
    now apply inst_ctxmap.
  Qed.
  Hint Resolve inst_ctxmap_up : pcuic.

Untyped renamings
  Definition renaming Γ Δ r :=
     x, match nth_error Γ x with
              | Some d
                match decl_body d return Prop with
                | Some b
                   b', option_map decl_body (nth_error Δ (r x)) = Some (Some b')
                             b'.[↑^(S (r x))] = b.[↑^(S x) s ren r]
                
                | Noneoption_map decl_body (nth_error Δ (r x)) = Some None
                end
              | Nonenth_error Δ (r x) = None
              end.

  Instance renaming_ext Γ Δ : Morphisms.Proper (`=1` ==> iff)%signature (renaming Γ Δ).
  Proof using Type.
    red. red. intros.
    split; intros.
    - intros n. specialize (H0 n).
      destruct nth_error; auto.
      destruct c as [na [b|] ty]; simpl in *; auto.
      destruct H0 as [b' [Heq Heq']]; auto. b'. rewrite -(H n).
      intuition auto. now rewrite Heq' H. now rewrite -H.
      now rewrite -H.
    - intros n. specialize (H0 n).
      destruct nth_error; auto.
      destruct c as [na [b|] ty]; simpl in *; auto.
      destruct H0 as [b' [Heq Heq']]; auto. b'. rewrite (H n).
      intuition auto. now rewrite Heq' H. now rewrite H.
      now rewrite H.
  Qed.

  Lemma shiftn1_renaming Γ Δ c c' r :
    renaming Γ Δ r
    (decl_body c' = option_map (fun xx.[ren r]) (decl_body c))
    renaming (c :: Γ) (c' :: Δ) (shiftn 1 r).
  Proof using Type.
    intros.
    red.
    destruct x. simpl.
    destruct (decl_body c) eqn:Heq; rewrite H0; auto. eexists. simpl. split; eauto.
    sigma. rewrite -ren_shiftn. now sigma.

    simpl.
    rewrite Nat.sub_0_r. specialize (H x).
    destruct nth_error eqn:Heq.
    destruct c0 as [na [b|] ty]; cbn in ×.
    destruct H as [b' [Hb Heq']].
     b'; intuition auto.
    rewrite -ren_shiftn. autorewrite with sigma in Heq' |- ×.
    rewrite Nat.sub_0_r.
    rewrite -?subst_compose_assoc -inst_assoc.
    rewrite -[b.[_]]inst_assoc. rewrite Heq'.
    now sigma.
    auto. auto.
  Qed.

  Lemma shift_renaming Γ Δ ctx ctx' r :
    All2i_len (fun n decl decl' ⇒ (decl_body decl' = option_map (fun xx.[ren (shiftn n r)]) (decl_body decl)))
          ctx ctx'
    renaming Γ Δ r
    renaming (Γ ,,, ctx) (Δ ,,, ctx') (shiftn #|ctx| r).
  Proof using Type.
    induction 1.
    intros. rewrite shiftn0. apply H.
    intros. simpl.
    rewrite shiftnS. apply shiftn1_renaming. apply IHX; try lia. auto.
    apply r0.
  Qed.

  Lemma shiftn_renaming Γ Δ ctx r :
    renaming Γ Δ r
    renaming (Γ ,,, ctx) (Δ ,,, rename_context r ctx) (shiftn #|ctx| r).
  Proof using Type.
    induction ctx; simpl; auto.
    × intros. rewrite shiftn0. apply H.
    × intros. simpl.
      rewrite shiftnS rename_context_snoc /=.
      apply shiftn1_renaming. now apply IHctx.
      simpl. destruct (decl_body a) ⇒ /= //.
      now sigma.
  Qed.

  Lemma shiftn_renaming_eq Γ Δ ctx r k :
    renaming Γ Δ r
    k = #|ctx|
    renaming (Γ ,,, ctx) (Δ ,,, rename_context r ctx) (shiftn k r).
  Proof using Type.
    now intros hr ->; apply shiftn_renaming.
  Qed.

  Lemma renaming_shift_rho_fix_context:
     (mfix : mfixpoint term) (Γ Δ : list context_decl) (r : nat nat),
      renaming Γ Δ r
      renaming (Γ ,,, rho_fix_context Γ mfix)
               (Δ ,,, rho_fix_context Δ (map (map_def (rename r) (rename (shiftn #|mfix| r))) mfix))
               (shiftn #|mfix| r).
  Proof using Type.
    intros mfix Γ Δ r Hr.
    rewrite -{2}(rho_fix_context_length Γ mfix).
    eapply shift_renaming; auto.
    rewrite /rho_fix_context !fold_fix_context_rev.
    apply All2i_rev_ctx_inv, All2i_mapi.
    simpl. apply All2i_trivial; auto. now rewrite map_length.
  Qed.

  Lemma map_fix_rho_rename:
     (mfix : mfixpoint term) (i : nat) (l : list term),
      ( t' : term, depth t' < depth (mkApps (tFix mfix i) l)
                     (Γ Δ : list context_decl) (r : nat nat) (P : nat bool),
            renaming Γ Δ r
            on_free_vars P t'
            rename r (rho Γ t') = rho Δ (rename r t'))
       (Γ Δ : list context_decl) (r : nat nat) P n,
        renaming Γ Δ r
        on_free_vars P (tFix mfix n)
         map (map_def (rename r) (rename (shiftn #|mfix| r)))
              (map_fix rho Γ (fold_fix_context rho Γ [] mfix) mfix) =
          map_fix rho Δ (fold_fix_context rho Δ [] (map (map_def (rename r) (rename (shiftn #|mfix| r))) mfix))
                  (map (map_def (rename r) (rename (shiftn #|mfix| r))) mfix).
  Proof using Type.
    intros mfix i l H Γ Δ r P H2 Hr onfix. inv_on_free_vars.
    rewrite /map_fix !map_map_compose !compose_map_def.
    apply map_ext_ind hin.
    have hdepth := mfixpoint_depth_In hin.
    eapply All_In in onfix as []; tea.
    move/andP: H0 ⇒ [onty onbod].
    apply map_def_eq_spec.
    - specialize (H (dtype d)).
      forward H. move: (depth_mkApps (tFix mfix i) l). simpl. lia.
      now eapply H; tea.
    - specialize (H (dbody d)).
      forward H. move: (depth_mkApps (tFix mfix i) l). simpl. lia.
      eapply H. eapply renaming_shift_rho_fix_context; tea. tea.
  Qed.

  Lemma All_IH {A depth} (l : list A) k (P : A Type) :
    list_depth_gen depth l < k
    ( x, depth x < k P x)
    All P l.
  Proof using Type.
    induction l in k |- ×. constructor.
    simpl. intros Hk IH.
    constructor. apply IH. lia.
    eapply (IHl k). lia. intros x sx.
    apply IH. lia.
  Qed.

  Lemma All_IH' {A depth B depth'} (f : A B) (l : list A) k (P : B Type) :
    list_depth_gen depth l < k
    ( x, depth' (f x) depth x)
    ( x, depth' x < k P x)
    All (fun xP (f x)) l.
  Proof using Type.
    induction l in k |- ×. constructor.
    simpl. intros Hk Hs IH.
    constructor. apply IH. specialize (Hs a). lia.
    eapply (IHl k). lia. apply Hs.
    apply IH.
  Qed.

  Transparent fold_context.

  Lemma fold_context_mapi_context f g (Γ : context) :
    fold_context f (mapi_context g Γ) =
    fold_context (fun Γf Γ map_decl (g #|Γ|)) Γ.
  Proof using Type.
    induction Γ. simpl. auto.
    simpl. f_equal; auto.
    now rewrite -IHΓ; len.
  Qed.

  Lemma mapi_context_fold_context f g (Γ : context) :
    mapi_context f (fold_context (fun Γg (mapi_context f Γ)) Γ) =
    fold_context (fun Γmap_decl (f #|Γ|) g Γ) Γ.
  Proof using Type.
    induction Γ. simpl. auto.
    simpl. f_equal; auto. len.
    now rewrite -IHΓ.
  Qed.

  Lemma onctx_fold_context_term P Γ (f g : context term term) :
    onctx P Γ
    ( Γ x,
      onctx P Γ
      fold_context_term f Γ = fold_context_term g Γ
      P x f (fold_context_term f Γ) x = g (fold_context_term g Γ) x)
    fold_context_term f Γ = fold_context_term g Γ.
  Proof using Type.
    intros onc Hp. induction onc; simpl; auto.
    f_equal; auto.
    eapply map_decl_eq_spec; tea.
    intros. now apply Hp.
  Qed.

  Lemma rho_ctx_rename Γ r :
    fold_context_term (fun Γ' xrho Γ' (rename (shiftn #|Γ'| r) x)) Γ =
    rho_ctx (rename_context r Γ).
  Proof using Type.
    rewrite /rename_context.
    rewrite -mapi_context_fold.
    rewrite fold_context_mapi_context.
    now setoid_rewrite compose_map_decl.
  Qed.

  Lemma rename_rho_ctx {r ctx} :
    onctx
      (fun t : term
         (Γ Δ : list context_decl) (r : nat nat),
        renaming Γ Δ r rename r (rho Γ t) = rho Δ (rename r t))
      ctx
    rename_context r (rho_ctx ctx) =
    rho_ctx (rename_context r ctx).
  Proof using Type.
    intros onc.
    rewrite /rename_context - !mapi_context_fold.
    induction onc; simpl; eauto.
    f_equal; eauto.
    rewrite !compose_map_decl.
    eapply map_decl_eq_spec; tea ⇒ /= t.
    intros IH.
    erewrite IH.
    1: now rewrite -IHonc; len.
    rewrite mapi_context_fold.
    rewrite -/(rename_context r (rho_ctx l)).
    epose proof (shiftn_renaming [] [] (rho_ctx l) r).
    rewrite !app_context_nil_l in H. eapply H.
    now intros i; rewrite !nth_error_nil.
  Qed.

  Lemma ondecl_map (P : term Type) f (d : context_decl) :
    ondecl P (map_decl f d)
    ondecl (fun xP (f x)) d.
  Proof using Type.
    destruct d ⇒ /=; rewrite /ondecl /=.
    destruct decl_body ⇒ /= //.
  Qed.


  Lemma rename_rho_ctx_over {ctx} {Γ Δ r P p} :
    renaming Γ Δ r
    forallb (on_free_vars P) (pparams p)
    test_context_k (fun k : naton_free_vars (closedP k xpredT)) #|p.(pparams)| ctx
    onctx
      (fun t : term
         (Γ Δ : list context_decl) (r : nat nat) P,
        renaming Γ Δ r on_free_vars P t rename r (rho Γ t) = rho Δ (rename r t))
      (inst_case_context p.(pparams) p.(puinst) ctx)
    rename_context r (rho_ctx_over Γ (inst_case_context p.(pparams) p.(puinst) ctx)) =
    rho_ctx_over Δ (rename_context r (inst_case_context p.(pparams) p.(puinst) ctx)).
  Proof using Type.
    rewrite /inst_case_context.
    intros Hr onpars clc onc.
    rewrite /rename_context - !mapi_context_fold.
    induction ctx; simpl; eauto.
    move: clc ⇒ /= /andP [] clc clx.
    specialize (IHctx clc).
    move: onc. rewrite /inst_case_context subst_instance_cons subst_context_snoc /= ⇒ onc.
    depelim onc.
    f_equal; eauto.
    rewrite !compose_map_decl.
    eapply ondecl_map in o.
    eapply ondecl_map in o.
    eapply map_decl_eqP_spec; teat.
    cbn; intros IH onfv.
    rewrite Nat.add_0_r; len. len in IH.
    erewrite <-IH ⇒ //. specialize (IHctx onc).
    rewrite -IHctx.
    rewrite mapi_context_fold.
    rewrite -/(rename_context _ _).
    relativize #|ctx|.
    apply (shiftn_renaming _ _ (rho_ctx_over Γ _) r Hr). now len.
    eapply on_free_vars_subst_gen.
    2:erewrite on_free_vars_subst_instance; tea.
    rewrite /on_free_vars_terms.
    solve_all.
  Qed.

  Lemma context_assumptions_fold_context_term f Γ :
    context_assumptions (fold_context_term f Γ) = context_assumptions Γ.
  Proof using Type.
    induction Γ ⇒ /= //.
    destruct (decl_body a) ⇒ /= //; f_equal ⇒ //.
  Qed.
  Hint Rewrite context_assumptions_fold_context_term : len.

  Lemma mapi_context_rename r Γ :
    mapi_context (fun k : natrename (shiftn k r)) Γ =
    rename_context r Γ.
  Proof using Type. rewrite mapi_context_fold //. Qed.

  Lemma inspect_nth_error_rename {r brs u res} (eq : nth_error brs u = res) :
     prf,
      inspect (nth_error (rename_branches r brs) u) =
      exist (option_map (rename_branch r) res) prf.
  Proof using Type. simpl.
    rewrite nth_error_map eq. now eq_refl.
  Qed.

  Lemma pres_bodies_rename Γ Δ r ctx :
    renaming Γ Δ r
    All2i_len
      (fun (n : nat) (decl decl' : context_decl) ⇒
        decl_body decl' =
        option_map (fun x : termx.[ren (shiftn n r)]) (decl_body decl))
      (rho_ctx_over Γ ctx)
      (rename_context r (rho_ctx_over Γ ctx)).
  Proof using Type.
    intros Hr.
    induction ctx; simpl; auto.
    - constructor.
    - rewrite rename_context_snoc. constructor; auto.
      destruct a as [na [b|] ty] ⇒ /= //.
      f_equal. now sigma.
  Qed.

  Lemma pres_bodies_rename' Γ Δ r ctx :
    renaming Γ Δ r
    All2i_len
      (fun (n : nat) (decl decl' : context_decl) ⇒
        decl_body decl' =
        option_map (fun x : termx.[ren (shiftn n r)]) (decl_body decl))
      ctx
      (rename_context r ctx).
  Proof using Type.
    intros Hr.
    induction ctx; simpl; auto.
    - constructor.
    - rewrite rename_context_snoc. constructor; auto.
      destruct a as [na [b|] ty] ⇒ /= //.
      f_equal. now sigma.
  Qed.

  Lemma rho_rename_pred Γ Δ p r P :
    renaming Γ Δ r
    forallb (on_free_vars P) (pparams p)
    on_free_vars (shiftnP #|pcontext p| P) (preturn p)
    test_context_k (fun k : natPCUICOnFreeVars.on_free_vars (PCUICOnFreeVars.closedP k xpredT))
      #|pparams p| (pcontext p)
    CasePredProp_depth
      (fun t : term
       (Γ Δ : list context_decl) (r : nat nat) P,
      renaming Γ Δ r on_free_vars P t rename r (rho Γ t) = rho Δ (rename r t)) p
    rename_predicate r (rho_predicate Γ p) = rho_predicate Δ (rename_predicate r p).
  Proof using Type.
    intros Hr onpars onret onp [? [? ?]].
    rewrite /rename_predicate /rho_predicate; cbn. f_equal. solve_all.
    eapply e. relativize #|pcontext p|; [eapply shift_renaming|]; tea; len ⇒ //.
    assert ((map (rho Δ) (map (rename r) (pparams p)) = map (rename r) (map (rho Γ) (pparams p)))).
    solve_all. erewrite b; trea.
    rewrite H.
    rewrite -rename_inst_case_context_wf //. len ⇒ //.
    rewrite /id. eapply pres_bodies_rename' ⇒ //; tea. tea.
  Qed.

  Lemma rename_rho_iota_red Γ Δ r p P pars args brs br c :
    renaming Γ Δ r
    #|args| = pars + context_assumptions br.(bcontext)
    forallb (on_free_vars P) (pparams p)
    closedn_ctx #|pparams p| br.(bcontext)
    on_free_vars (shiftnP #|bcontext br| P) (bbody br)
    test_context_k (fun k : naton_free_vars (closedP k xpredT)) #|pparams p| (bcontext br)
    CasePredProp_depth
    (fun t : term
     (Γ Δ : list context_decl) (r : nat nat) P,
    renaming Γ Δ r on_free_vars P t rename r (rho Γ t) = rho Δ (rename r t)) p
    CaseBrsProp_depth p
      (fun t : term
       (Γ Δ : list context_decl) (r : nat nat) P,
      renaming Γ Δ r on_free_vars P t rename r (rho Γ t) = rho Δ (rename r t)) brs
    nth_error brs c = Some br
    rename r (rho_iota_red Γ (rho_predicate Γ p) pars args br) =
    rho_iota_red Δ (rho_predicate Δ (rename_predicate r p)) pars (map (rename r) args) (rename_branch r br).
  Proof using Type.
    intros Hr hlen hpars hlen' hbod hbr hpred hbrs hnth.
    unfold rho_iota_red.
    rewrite rename_subst0 map_rev map_skipn. f_equal.
    rewrite List.rev_length /expand_lets /expand_lets_k.
    rewrite rename_subst0. len.
    rewrite skipn_length; try lia.
    rewrite hlen.
    replace (pars + context_assumptions (bcontext br) - pars)
      with (context_assumptions (bcontext br)) by lia.
    rewrite shiftn_add Nat.add_comm rename_shiftnk.
    relativize (context_assumptions _); [erewrite rename_extended_subst|now len].
    assert ((map (rho Δ) (map (rename r) (pparams p)) = map (rename r) (map (rho Γ) (pparams p)))).
    destruct hpred as [? _].
    solve_all. erewrite b; trea.
    f_equal. f_equal. rewrite /inst_case_branch_context /= /id.
    rewrite H.
    rewrite -rename_inst_case_context_wf // /id. len ⇒ //.
    eapply All_nth_error in hbrs as []; tea.
    f_equal.
    rewrite /inst_case_branch_context. cbn.
    erewrite e; trea.
    relativize #|bcontext br|; [eapply shift_renaming|]; tea; len ⇒ //.
    rewrite H -rename_inst_case_context_wf //. now len.
    rewrite /id. now eapply pres_bodies_rename'.
  Qed.

  Lemma rho_rename P Γ Δ r t :
    renaming Γ Δ r
    on_free_vars P t
    rename r (rho Γ t) = rho Δ (rename r t).
  Proof using cf Σ wfΣ.
    revert t Γ Δ r P.
    refine (PCUICDepth.term_ind_depth_app _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _);
      intros until Γ; intros Δ r P Hr ont; try subst Γ; try rename Γ0 into Γ; repeat inv_on_free_vars.
    all:auto 2.

    - red in Hr. simpl.
      specialize (Hr n).
      destruct (nth_error Γ n) as [c|] eqn:Heq.
      -- simp rho. rewrite Heq /=.
         destruct decl_body eqn:Heq''.
         simp rho. rewrite lift0_inst.
         destruct Hr as [b' [-> Hb']] ⇒ /=.
         rewrite lift0_inst.
         sigma. autorewrite with sigma in ×. now rewrite <- Hb'.
         simpl.
         rewrite Hr. simpl. reflexivity.

      -- simp rho. rewrite Heq Hr //.

    - simpl; simp rho. simpl. f_equal; rewrite !map_map_compose. solve_all.

    - simpl; simp rho; simpl. erewrite H; eauto. f_equal.
      erewrite H0; eauto.
      simpl. eapply (shift_renaming _ _ [_] [_]). repeat constructor. auto.

    - simpl; simp rho; simpl. erewrite H; eauto.
      erewrite H0; eauto.
      simpl. eapply (shift_renaming _ _ [_] [_]). repeat constructor. auto.

    - simpl; simp rho; simpl. rewrite /subst1 subst_inst.
      specialize (H _ _ _ _ Hr p). specialize (H0 _ _ _ _ Hr p0).
      autorewrite with sigma in H, H0, H1.
      erewrite <- (H1 ((vdef n (rho Γ t) (rho Γ t0) :: Γ))).
      2:{ eapply (shift_renaming _ _ [_] [_]). repeat constructor. simpl.
          sigma. now rewrite -H. auto. }
      sigma. apply inst_ext. rewrite H.
      rewrite -ren_shiftn. sigma. unfold Up. now sigma. tea.

    - rewrite rho_equation_8.
      destruct (view_lambda_fix_app t u); try inv_on_free_vars.

      +
        rename b into onfvb. rename a into onfvfix. rename a0 into a.
        simpl; simp rho. rewrite rename_mkApps. cbn [rename].
        assert (eqargs : map (rename r) (map (rho Γ) (l ++ [a])) =
                map (rho Δ) (map (rename r) (l ++ [a]))).
        { rewrite !map_map_compose !map_app. f_equal ⇒ /= //.
          2:{ f_equal. now eapply H1. }
          unshelve epose proof (All_IH l _ _ _ H); simpl; eauto.
          pose proof (depth_mkApps (tFix mfix i) l). lia. solve_all. }
        destruct (rho_fix_elim Γ mfix i (l ++ [a])).
        simpl. simp rho.
        rewrite /unfold_fix /map_fix nth_error_map e /= i0.
        simp rho; rewrite /map_fix !nth_error_map /= e /=.
        move: i0; rewrite /is_constructor -(map_app (rename r) l [a]) nth_error_map.
        destruct (nth_error_spec (l ++ [a]) (rarg d)) ⇒ /= //.
        rewrite -isConstruct_app_rename ⇒ → //.
        rewrite rename_mkApps.
        f_equal; auto.
        assert (Hbod: (Γ Δ : list context_decl) (r : nat nat),
                   renaming Γ Δ r rename r (rho Γ (dbody d)) = rho Δ (rename r (dbody d))).
        { pose proof (H (dbody d)) as Hbod.
          forward Hbod.
          { simpl; move: (depth_mkApps (tFix mfix i) l). simpl.
            eapply mfixpoint_depth_nth_error in e. lia. }
          auto. intros. eapply Hbod; tea.
          inv_on_free_vars. eapply All_nth_error in onfvfix; tea.
          now move/andP: onfvfix. }
        assert (Hren : renaming (Γ ,,, rho_fix_context Γ mfix)
                           (Δ ,,, rho_fix_context Δ (map (map_def (rename r) (rename (shiftn #|mfix| r))) mfix))
                           (shiftn #|mfix| r)).
        now apply renaming_shift_rho_fix_context.
        specialize (Hbod _ _ _ Hren).
        rewrite -Hbod.
        rewrite !subst_inst.
        { sigma. eapply inst_ext.
          rewrite -{1}(rename_inst r).
          rewrite -ren_shiftn. sigma.
          rewrite Upn_comp ?map_length ?fix_subst_length ?map_length //.
          apply subst_consn_proper ⇒ //.
          rewrite map_fix_subst //.
          intros n. simp rho. simpl. simp rho.
          reflexivity.
          clear -H Hr Hren onfvfix.
          unfold fix_subst. autorewrite with len. generalize #|mfix| at 1 4.
          induction n; simpl; auto.
          rewrite IHn. clear IHn. f_equal; auto.
          specialize (H (tFix mfix n)) as Hbod.
          forward Hbod.
          { simpl. move: (depth_mkApps (tFix mfix i) l). simpl. lia. }
          simp rho. simpl. simp rho.
          specialize (Hbod _ _ _ _ Hr onfvfix).
          simpl in Hbod. simp rho in Hbod.
          simpl in Hbod; simp rho in Hbod.
          rewrite -rename_inst.
          rewrite ren_shiftn -(rename_inst (shiftn _ r)).
          rewrite Hbod. f_equal.
          rewrite /map_fix !map_map_compose. apply map_ext.
          intros []; unfold map_def; cbn. f_equal.
          f_equal. 2:rewrite -up_Upn ren_shiftn. 2:now sigma.
          f_equal. f_equal.
          apply map_extx. f_equal.
          now rewrite -up_Upn ren_shiftn; sigma. }

        simp rho; simpl; simp rho.
        rewrite /unfold_fix /map_fix !nth_error_map.
        destruct (nth_error mfix i) eqn:hfix ⇒ /=.
        assert(is_constructor (rarg d) (l ++ [a]) = false).
        red in i0; unfold negb in i0.
        destruct is_constructor; auto.
        rewrite H2.
        rewrite -(map_app (rename r) l [a]) -is_constructor_rename H2 //.
        rewrite rename_mkApps.
        f_equal. simpl. f_equal.
        autorewrite with len.
        eapply (map_fix_rho_rename mfix i l); eauto.
        intros. eapply H; eauto. rewrite /=. lia.
        apply eqargs.
        rewrite rename_mkApps. f_equal; auto.
        2:{ now rewrite -(map_app (rename r) _ [_]). }
        simpl. f_equal. autorewrite with len.
        eapply (map_fix_rho_rename mfix i l); eauto.
        intros; eapply H; tea; simpl; try lia.

      +
        inv_on_free_vars. rename a0 into arg. rename b0 into body.
        pose proof (rho_app_lambda' Γ na ty body (l ++ [arg])).
        simp rho in H2. rewrite mkApps_app in H2.
        simpl in H2. simp rho in H2. rewrite {}H2.
        simpl.
        rewrite rename_mkApps. simpl.
        rewrite tApp_mkApps -mkApps_app.
        rewrite -(map_app (rename r) _ [_]).
        rewrite rho_app_lambda'.
        simpl.
        assert (All (fun xrename r (rho Γ x) = rho Δ (rename r x)) (l ++ [arg])).
        { apply All_app_inv. 2:constructor; auto.
          unshelve epose proof (All_IH l _ _ _ H); simpl; eauto.
          move: (depth_mkApps (tLambda na ty body) l). lia. solve_all.
          eapply H1; tea. }
        remember (l ++ [arg]) as args.
        destruct args; simpl; simp rho.
        { apply (f_equal (@length _)) in Heqargs. simpl in Heqargs.
         autorewrite with len in Heqargs. simpl in Heqargs. lia. }
        rewrite rename_inst /subst1 subst_inst.
        simpl in H.
        specialize (H body).
        forward H.
        { move: (depth_mkApps (tLambda na ty body) l) ⇒ /=. lia. }
        rewrite inst_mkApps.
        specialize (H (vass na (rho Γ ty) :: Γ) (vass na (rho Δ ty.[ren r]) :: Δ) (shiftn 1 r) (shiftnP 1 P)).
        forward H. eapply shiftn1_renaming; auto.
        sigma. depelim X.
        autorewrite with sigma in H, e, X.
        f_equal.
        rewrite -H //. sigma. apply inst_ext.
        rewrite e.
        rewrite -ren_shiftn. sigma.
        unfold Up. now sigma.
        rewrite !map_map_compose. solve_all.
        now autorewrite with sigma in H.
      + simpl.
        simp rho. pose proof (isFixLambda_app_rename r _ i).
        simpl in H2. rewrite (view_lambda_fix_app_other (rename r t) (rename r a0) H2). simpl.
        erewrite H0, H1; eauto.

    -
      simpl; simp rho; simpl.
      case e: lookup_env ⇒ [[decl|decl]|] //; simp rho.
      case eb: cst_body ⇒ [b|] //; simp rho.
      rewrite rename_inst inst_closed0 //.
      apply declared_decl_closed in e ⇒ //.
      hnf in e. rewrite eb in e. rewrite closedn_subst_instance; auto.
      now move/andP: e ⇒ [-> _].

    -
      simpl; simp rho.
      destruct inspect as [[f a] decapp].
      destruct inspect as [[f' a'] decapp'].
      epose proof (decompose_app_rename decapp).
      rewritedecapp' in H0. noconf H0.
      simpl.
      assert (map (rename_branch r) (map (rho_br Γ (rho_predicate Γ p)) brs) =
              (map (rho_br Δ (rho_predicate Δ (rename_predicate r p))) (map (rename_branch r) brs))).
      { destruct X as [? [? ?]]; red in X0.
        simpl in ×. rewrite !map_map_compose /rename_branch
          /PCUICSigmaCalculus.rename_branch /rho_br /=.
        simpl. solve_all. f_equal.
        rewrite /inst_case_branch_context /=.
        eapply All_prod_inv in p0 as [].
        unshelve epose proof (rename_rho_ctx_over Hr _ _ a2). shelve. solve_all. solve_all.
        erewrite b0. reflexivity.
        assert (map (rho Δ) (map (rename r) (pparams p)) = (map (rename r) (map (rho Γ) ((pparams p))))).
        solve_all. erewrite a0; trea. rewrite H3.
        rewrite - rename_inst_case_context_wf //.
        len ⇒ //.
        eapply shiftn_renaming_eq ⇒ //. now len. tea. }

      simpl.
      destruct X as [? [? ?]]; cbn in ×. red in X0.
      destruct view_construct_cofix; simpl; simp rho.

      × destruct (eq_inductive ci ind) eqn:eqi.
        simp rho.
        destruct inspect as [[br|] eqbr]=> //; simp rho;
        destruct (inspect_nth_error_rename (r:=r) eqbr) as [prf ->]; simp rho.
        cbv zeta. simp rho.
        cbn -[eqb]. autorewrite with len.
        case: eqb_specT ⇒ // hlen.
        + erewrite rename_rho_iota_red; tea ⇒ //.
          f_equal.
          pose proof (decompose_app_inv decapp). subst t.
          specialize (H _ _ _ _ Hr p3).
          rewrite /= !rho_app_construct /= !rename_mkApps in H.
          simpl in H. rewrite rho_app_construct in H.
          apply mkApps_eq_inj in H as [_ Heq] ⇒ //.
          len; eauto.
          { cbn. len. eapply nth_error_forallb in p4; tea.
            move: p4 ⇒ /= /andP[]. rewrite test_context_k_closed_on_free_vars_ctx.
            now rewrite closedn_ctx_on_free_vars. }
          eapply nth_error_forallb in p4; tea. cbn in p4.
          now move/andP: p4.
          eapply nth_error_forallb in p4; tea. cbn in p4.
          now move/andP: p4.
        + simp rho. simpl. f_equal; auto.
          erewriterho_rename_pred; tea ⇒ //.
          erewrite H; trea.
        + simp rho. simpl. f_equal; eauto.
          erewriterho_rename_pred; tea ⇒ //.
          simp rho.
        + simp rho. simpl. simp rho. f_equal; eauto.
          erewriterho_rename_pred; tea ⇒ //.

      × simpl; simp rho.
        rewrite /map_fix !map_map_compose.
        rewrite /unfold_cofix !nth_error_map.
        apply decompose_app_inv in decapp. subst t.
        specialize (H _ _ _ _ Hr p3).
        simp rho in H; rewrite !rename_mkApps /= in H. simp rho in H.
        eapply mkApps_eq_inj in H as [Heqcof Heq] ⇒ //.
        noconf Heqcof. simpl in H.
        autorewrite with len in H.
        rewrite /map_fix !map_map_compose in H.

        case efix: (nth_error mfix idx) ⇒ [d|] /= //.
        + rewrite rename_mkApps !map_map_compose compose_map_def.
          f_equal. erewriterho_rename_pred; tea ⇒ //.
          rewrite !map_map_compose in Heq.
          f_equal ⇒ //.
          rewrite !subst_inst. sigma.
          apply map_eq_inj in H.
          epose proof (nth_error_all efix H). cbn in H1.
          simpl in H1. apply (f_equal dbody) in H1.
          simpl in H1. rewrite -(rename_inst (shiftn _ r)) -(rename_inst r).
          rewrite -H1. sigma.
          apply inst_ext.
          rewrite -ren_shiftn. sigma.
          (rewrite Upn_comp ?map_length ?fix_subst_length ?map_length //;
            try now autorewrite with len); [].
          apply subst_consn_proper ⇒ //.
          rewrite map_cofix_subst' //.
          intros n'; simp rho. simpl; f_equal. now simp rho.
          rewrite map_cofix_subst' //.
          simpl. moven'; f_equal. simp rho; simpl; simp rho.
          f_equal. rewrite /map_fix.
          rewrite !map_map_compose !compose_map_def.
          apply map_extx; apply map_def_eq_spec ⇒ //.
          rewrite !map_map_compose.
          unfold cofix_subst. generalize #|mfix|.
          clear -H.
          induction n; simpl; auto. f_equal; auto.
          simp rho. simpl. simp rho. f_equal.
          rewrite /map_fix !map_map_compose. autorewrite with len.
          solve_all.
          apply (f_equal dtype) in H. simpl in H.
          now sigma; sigma in H. sigma.
          rewrite -ren_shiftn. rewrite up_Upn.
          apply (f_equal dbody) in H. simpl in H.
          sigma in H. now rewrite <-ren_shiftn, up_Upn in H.
          now rewrite !map_map_compose in H0.

        + rewrite map_map_compose. f_equal; auto.
          { erewriterho_rename_pred; tea ⇒ //. }
          { simp rho. rewrite !rename_mkApps /= !map_map_compose !compose_map_def /=.
            simp rho. f_equal. f_equal.
            rewrite /map_fix map_map_compose. rewrite -H.
            autorewrite with len. reflexivity.
            now rewrite -Heq !map_map_compose. }
        now rewrite !map_map_compose in H0.
      × pose proof (construct_cofix_rename r t0 d).
        destruct (view_construct_cofix (rename r t0)); simpl in H1 ⇒ //.
        simp rho. simpl.
        f_equal; auto.
        erewrite rho_rename_pred; tea⇒ //.
        now rewrite !map_map_compose in H0. simp rho.

    -
      simpl.
      rewrite !rho_app_proj.
      destruct decompose_app as [f a] eqn:decapp.
      erewrite (decompose_app_rename decapp).
      erewrite <-H; eauto.
      apply decompose_app_inv in decapp. subst t.
      specialize (H _ _ _ _ Hr ont).
      rewrite rename_mkApps in H.

      destruct f; simpl; auto.
      × destruct n; simpl; auto.
        destruct eq_inductive eqn:eqi; simpl; auto.
        rewrite nth_error_map.
        destruct nth_error eqn:hnth; simpl; auto.
        simp rho in H. rewrite rename_mkApps in H.
        eapply mkApps_eq_inj in H as [_ Hargs] ⇒ //.
        rewrite !map_map_compose in Hargs.
        eapply map_eq_inj in Hargs.
        apply (nth_error_all hnth Hargs).
      × rewrite nth_error_map.
        destruct nth_error eqn:hnth; auto.
        simpl. rewrite rename_mkApps.
        f_equal; auto.
        simpl in H; simp rho in H. rewrite rename_mkApps in H.
        eapply mkApps_eq_inj in H as [Hcof Hargs] ⇒ //.
        f_equal; auto. simpl in Hcof. noconf Hcof. simpl in H.
        noconf H.
        rewrite /map_fix !map_map_compose in H.
        apply map_eq_inj in H.
        epose proof (nth_error_all hnth H).
        simpl in H0. apply (f_equal dbody) in H0.
        simpl in H0. autorewrite with sigma in H0.
        rewrite !rename_inst -H0 - !rename_inst.
        sigma. autorewrite with len.
        apply inst_ext.
        rewrite -ren_shiftn. sigma.
        (rewrite Upn_comp ?map_length ?fix_subst_length ?map_length //;
          try now autorewrite with len); [].
        apply subst_consn_proper ⇒ //.
        rewrite map_cofix_subst' //.
        intros n0. simpl. now rewrite up_Upn.
        rewrite !map_map_compose.
        unfold cofix_subst. generalize #|mfix|.
        clear -H.
        induction n; simpl; auto. f_equal; auto.
        simp rho. simpl. simp rho. f_equal.
        rewrite /map_fix !map_map_compose. autorewrite with len.
        eapply All_map_eq, All_impl; tea ⇒ /= //.
        intros x.
        rewrite !rename_inst ren_shiftn ⇒ <-.
        apply map_def_eq_spec; simpl. now sigma. sigma. now len.

    -
      simpl; simp rho; simpl; simp rho.
      f_equal. rewrite /map_fix !map_length !map_map_compose.
      red in X0. solve_all.
      move/andP: b ⇒ [] onty onbody.
      erewrite a0; tea; auto.
      move/andP: b ⇒ [] onty onbody.
      assert (#|m| = #|fold_fix_context rho Γ [] m|). rewrite fold_fix_context_length /= //.
      erewrite <-b0; trea.
      rewrite {2}H.
      eapply shift_renaming; auto.
      clear. generalize #|m|. induction m using rev_ind. simpl. constructor.
      intros. rewrite map_app !fold_fix_context_app. simpl. constructor. simpl. reflexivity. apply IHm.

    -
      simpl; simp rho; simpl; simp rho.
      f_equal. rewrite /map_fix !map_length !map_map_compose.
      red in X0. solve_all.
      move/andP: b ⇒ [] onty onbody.
      erewrite a0; tea; auto.
      move/andP: b ⇒ [] onty onbody.
      assert (#|m| = #|fold_fix_context rho Γ [] m|). rewrite fold_fix_context_length /= //.
      erewrite <-b0; trea.
      rewrite {2}H.
      eapply shift_renaming; auto.
      clear. generalize #|m|. induction m using rev_ind. simpl. constructor.
      intros. rewrite map_app !fold_fix_context_app. simpl. constructor. simpl. reflexivity. apply IHm; eauto.
  Qed.

  Lemma rho_lift0 Γ Δ P t :
    on_free_vars P t
    lift0 #|Δ| (rho Γ t) = rho (Γ ,,, Δ) (lift0 #|Δ| t).
  Proof using wfΣ.
    rewrite !lift_rename. eapply rho_rename.
    red. intros x. destruct nth_error eqn:Heq.
    unfold lift_renaming. simpl. rewrite Nat.add_comm.
    rewrite nth_error_app_ge. lia. rewrite Nat.add_sub Heq.
    destruct c as [na [b|] ty]; simpl in *; auto.
     b. split; eauto.
    rewrite -ren_shiftk. rewrite shiftk_compose. reflexivity.
    unfold lift_renaming. simpl. rewrite Nat.add_comm.
    rewrite nth_error_app_ge. lia. now rewrite Nat.add_sub Heq.
  Qed.

  Lemma rho_ctx_over_app Γ' Γ Δ :
    rho_ctx_over Γ' (Γ ,,, Δ) =
    rho_ctx_over Γ' Γ ,,, rho_ctx_over (Γ' ,,, rho_ctx_over Γ' Γ) Δ.
  Proof using Type.
    induction Δ; simpl; auto.
    destruct a as [na [b|] ty]. simpl. f_equal; auto.
    now rewrite IHΔ app_context_assoc.
    now rewrite IHΔ app_context_assoc.
  Qed.

  Lemma rho_ctx_app Γ Δ : rho_ctx (Γ ,,, Δ) = rho_ctx Γ ,,, rho_ctx_over (rho_ctx Γ) Δ.
  Proof using Type.
    induction Δ; simpl; auto.
    destruct a as [na [b|] ty]; simpl; f_equal; auto.
    now rewrite -IHΔ.
    now rewrite -IHΔ.
  Qed.

  Lemma fold_fix_context_over_acc p Γ m acc :
    forallb (test_def (on_free_vars p) (on_free_vars (shiftnP #|m| p))) m
    rho_ctx_over (Γ ,,, acc)
      (List.rev (mapi_rec (fun (i : nat) (d : def term) ⇒ vass (dname d) ((lift0 i) (dtype d))) m #|acc|))
      ++ acc =
    fold_fix_context rho Γ acc m.
  Proof using wfΣ.
    generalize #|m|n.
    induction m in Γ, acc |- *; simpl; auto.
    move/andP ⇒ [] ha hm.
    rewrite rho_ctx_over_app. simpl.
    unfold app_context. unfold app_context in IHm.
    erewrite <- IHm ⇒ //.
    rewrite - app_assoc. cbn. f_equal.
    apply fold_context_Proper. intros Δ d.
    apply map_decl_extx.
    rewrite (rho_lift0 _ _ p); auto. now move/andP: ha.
    repeat f_equal. rewrite (rho_lift0 _ _ p); auto.
    now move/andP: ha.
  Qed.

  Lemma fold_fix_context_rho_ctx p Γ m :
    forallb (test_def (on_free_vars p) (on_free_vars (shiftnP #|m| p))) m
    rho_ctx_over Γ (fix_context m) =
    fold_fix_context rho Γ [] m.
  Proof using wfΣ.
    intros hm.
    rewrite <- (fold_fix_context_over_acc p); now rewrite ?app_nil_r.
  Qed.

  Definition fold_fix_context_alt Γ m :=
    mapi (fun k defvass def.(dname) (lift0 k (rho Γ def.(dtype)))) m.

  Lemma fix_context_fold p Γ m :
    forallb (test_def (on_free_vars p) (on_free_vars (shiftnP #|m| p))) m
    fix_context (map (map_def (rho Γ)
                              (rho (Γ ,,, rho_ctx_over Γ (fix_context m)))) m) =
    rho_ctx_over Γ (fix_context m).
  Proof using wfΣ.
    intros hm.
    unfold fix_context. rewrite mapi_map. simpl.
    rewrite (fold_fix_context_rho_ctx p); auto.
    rewrite fold_fix_context_rev_mapi. simpl.
    now rewrite app_nil_r.
  Qed.

  Lemma fix_context_map_fix p Γ mfix :
    forallb (test_def (on_free_vars p) (on_free_vars (shiftnP #|mfix| p))) mfix
    fix_context (map_fix rho Γ (rho_ctx_over Γ (fix_context mfix)) mfix) =
    rho_ctx_over Γ (fix_context mfix).
  Proof using wfΣ.
    intros hm.
    rewrite - (fix_context_fold p) //.
    unfold map_fix. f_equal.
    f_equal. f_equal. rewrite (fix_context_fold p) //.
  Qed.

  Lemma rho_cofix_subst p Γ mfix :
    forallb (test_def (on_free_vars p) (on_free_vars (shiftnP #|mfix| p))) mfix
    cofix_subst (map_fix rho Γ (rho_ctx_over Γ (fix_context mfix)) mfix)
    = (map (rho Γ) (cofix_subst mfix)).
  Proof using wfΣ.
    intros hm.
    unfold cofix_subst. unfold map_fix at 2. rewrite !map_length.
    induction #|mfix| at 1 2. reflexivity. simpl. simp rho. simpl.
    simp rho. rewrite - (fold_fix_context_rho_ctx p) //. f_equal. apply IHn.
  Qed.

  Lemma rho_fix_subst p Γ mfix :
    forallb (test_def (on_free_vars p) (on_free_vars (shiftnP #|mfix| p))) mfix
    fix_subst (map_fix rho Γ (rho_ctx_over Γ (fix_context mfix)) mfix)
    = (map (rho Γ) (fix_subst mfix)).
  Proof using wfΣ.
    intros hm. unfold fix_subst. unfold map_fix at 2. rewrite !map_length.
    induction #|mfix| at 1 2. reflexivity. simpl. simp rho; simpl; simp rho.
    rewrite -(fold_fix_context_rho_ctx p) //. f_equal. apply IHn.
  Qed.