Library MetaCoq.PCUIC.PCUICParallelReduction

Require Import RelationClasses CRelationClasses.
From MetaCoq.Template Require Import config utils.
From MetaCoq.PCUIC Require Import PCUICUtils PCUICOnOne PCUICAst PCUICAstUtils PCUICTactics PCUICDepth PCUICCases
     PCUICLiftSubst PCUICUnivSubst PCUICReduction PCUICTyping
     PCUICSigmaCalculus PCUICWeakeningEnvConv PCUICInduction
     PCUICRenameDef PCUICRenameConv PCUICInstDef PCUICInstConv PCUICOnFreeVars
     PCUICWeakeningConv PCUICWeakeningTyp PCUICSubstitution.

Require Import ssreflect ssrbool.
From Equations Require Import Equations.

Set Default Proof Using "Type*".

Local Set Keyed Unification.

Ltac simplify_IH_hyps :=
  repeat match goal with
      [ H : _ |- _ ] ⇒ eqns_specialize_eqs H
  end.

All2 lemmas

Definition All2_prop_eq Γ Γ' {A B} (f : A term) (g : A B) (rel : (Γ Γ' : context) (t t' : term), Type) :=
  All2 (on_Trel_eq (rel Γ Γ') f g).

Definition All2_prop Γ (rel : (Γ : context) (t t' : term), Type) :=
  All2 (rel Γ).


Lemma All2_All2_prop {P Q : context context term term Type} {par par'} {l l' : list term} :
  All2 (P par par') l l'
  ( x y, P par par' x y Q par par' x y)
  All2 (Q par par') l l'.
Proof.
  intros H aux.
  induction H; constructor. unfold on_Trel in ×.
  apply aux; apply r. apply IHAll2.
Defined.

Lemma All2_branch_prop {P Q : context context branch term branch term Type}
  {par par'} {l l' : list (branch term)} :
  All2 (P par par') l l'
  ( x y, P par par' x y Q par par' x y)
  All2 (Q par par') l l'.
Proof.
  intros H aux.
  induction H; constructor. unfold on_Trel in ×.
  apply aux; apply r. apply IHAll2.
Defined.

Lemma All2_All2_prop_eq {A B} {P Q : context context term term Type} {par par'}
      {f : A term} {g : A B} {l l' : list A} :
  All2 (on_Trel_eq (P par par') f g) l l'
  ( x y, P par par' x y Q par par' x y)
  All2_prop_eq par par' f g Q l l'.
Proof.
  intros H aux.
  induction H; constructor. unfold on_Trel in ×.
  split. apply aux; apply r. apply r. apply IHAll2.
Defined.

Definition All2_prop2_eq Γ Γ' Γ2 Γ2' {A B} (f g : A term) (h : A B)
           (rel : (Γ Γ' : context) (t t' : term), Type) :=
  All2 (fun x yon_Trel (rel Γ Γ') f x y × on_Trel_eq (rel Γ2 Γ2') g h x y)%type.

Definition All2_prop2 Γ Γ' {A} (f g : A term)
           (rel : (Γ : context) (t t' : term), Type) :=
  All2 (fun x yon_Trel (rel Γ) f x y × on_Trel (rel Γ') g x y)%type.

Lemma All2_All2_prop2_eq {A B} {P Q : context context term term Type} {par par' par2 par2'}
      {f g : A term} {h : A B} {l l' : list A} :
  All2_prop2_eq par par' par2 par2' f g h P l l'
  ( par par' x y, P par par' x y Q par par' x y)
  All2_prop2_eq par par' par2 par2' f g h Q l l'.
Proof.
  intros H aux.
  induction H; constructor. unfold on_Trel in ×. split.
  apply aux. destruct r. apply p. split. apply aux. apply r. apply r. apply IHAll2.
Defined.

Specialization of All2_fold to on_decls / All_decls. It compares contexts up to `P` and no alpha-equivalence.
Notation on_decls_over P Γ Γ' := (fun Δ Δ'P (Γ ,,, Δ) (Γ' ,,, Δ')).
Notation on_contexts_over P Γ Γ' := (All2_fold (on_decls (on_decls_over P Γ Γ'))).
Notation on_contexts_app := All2_fold_app.
Notation on_contexts_length := All2_fold_length.

Section All2_fold.

Do not change this definition as it is used in a raw fixpoint so should preserve the guard condition.
  Lemma on_contexts_impl {P Q : context context term term Type} {par par'} :
    on_contexts P par par'
    ( par par' x y, P par par' x y Q par par' x y)
    on_contexts Q par par'.
  Proof.
    intros H aux.
    induction H; constructor; tas.
    destruct p; constructor.
    apply aux, p. apply aux, p. apply aux, p0.
  Defined.

  Lemma on_contexts_impl_ind {P Q : context context term term Type} {par par'} :
    on_contexts P par par'
    ( par par' x y,
      on_contexts Q par par'
      P par par' x y Q par par' x y)
    on_contexts Q par par'.
  Proof.
    intros H aux.
    induction H; constructor; auto. eapply All_decls_impl; tea. eauto.
  Qed.

  Lemma on_contexts_app':
     P (Γ Γ' Γ'' : context),
      on_contexts P (Γ ,,, Γ') Γ''
       Γl Γr, (Γ'' = Γl ,,, Γr) #|Γ'| = #|Γr| #|Γ| = #|Γl|.
  Proof.
    intros ×.
    revert Γ''. induction Γ'. simpl. intros.
     Γ'', []. intuition auto. eapply (on_contexts_length X).
    intros. unfold app_context in X. depelim X.
    destruct (IHΓ' _ X) as [Γl [Γr [Heq HeqΓ]]]. subst Γ'0.
    eexists Γl, (Γr,, d'). simpl. intuition eauto. lia.
  Qed.

  Lemma on_contexts_app_ex:
     P (Γ Γ' Γ'' : context),
      on_contexts P (Γ ,,, Γ') Γ''
       Γl Γr, (Γ'' = Γl ,,, Γr) ×
      All2_fold
        (on_decls P)
        Γ Γl × All2_fold (on_decls (fun Δ Δ'P (Γ ,,, Δ) (Γl ,,, Δ'))) Γ' Γr.
  Proof.
    intros ×.
    revert Γ''. induction Γ'. simpl. intros.
     Γ'', []. intuition auto. constructor.
    intros. unfold app_context in X. depelim X.
    destruct (IHΓ' _ X) as [Γl [Γr [[HeqΓ H2] H3]]]. subst.
    eexists _, _. intuition eauto. unfold snoc, app_context.
    now rewrite app_comm_cons. constructor; auto.
  Qed.

  Lemma on_contexts_app_inv :
     P (Γ Γ' Γl Γr : context),
      on_contexts P (Γ ,,, Γ') (Γl ,,, Γr)
      #|Γ| = #|Γl|
      on_contexts P Γ Γl ×
      on_contexts (fun Δ Δ'P (Γ ,,, Δ) (Γl ,,, Δ')) Γ' Γr.
  Proof.
    intros × a hl.
    apply: All2_fold_app_inv ⇒ //.
    apply All2_fold_length in a. len in a.
  Qed.

  Lemma nth_error_pred1_ctx {P} {Γ Δ} i body' :
    on_contexts P Γ Δ
    option_map decl_body (nth_error Δ i) = Some (Some body')
    { body & (option_map decl_body (nth_error Γ i) = Some (Some body)) ×
             P (skipn (S i) Γ) (skipn (S i) Δ) body body' }%type.
  Proof.
    intros Hpred. revert i body'.
    induction Hpred; destruct i; try discriminate; auto; !intros.
    simpl in heq_option_map. depelim p ⇒ //.
    noconf heq_option_map. b. intuition eauto.
    specialize (IHHpred _ _ heq_option_map) as [body [Heq Hpred']].
    intuition eauto.
  Qed.

  Lemma nth_error_pred1_ctx_l {P} {Γ Δ} i body :
    on_contexts P Γ Δ
    option_map decl_body (nth_error Γ i) = Some (Some body)
    { body' & (option_map decl_body (nth_error Δ i) = Some (Some body')) ×
             P (skipn (S i) Γ) (skipn (S i) Δ) body body' }%type.
  Proof.
    intros Hpred. revert i body.
    induction Hpred; destruct i; try discriminate; auto; !intros.
    depelim p ⇒ //.
    noconf heq_option_map. b'. intuition eauto.
    simpl in heq_option_map. specialize (IHHpred _ _ heq_option_map) as [body' [Heq Hpred']].
    intuition eauto.
  Qed.

  Lemma on_contexts_over_app P {Γ0 Δ Γ'' Δ''} :
    on_contexts P Γ0 Δ
    on_contexts_over P Γ0 Δ Γ'' Δ''
    on_contexts P (Γ0 ,,, Γ'') (Δ ,,, Δ'').
  Proof.
    intros. induction X0; pcuic; constructor; pcuic.
  Qed.

  Lemma on_contexts_app_inv_left {P Γ Γ' Δ Δ'} :
    on_contexts P (Γ ,,, Δ) (Γ' ,,, Δ') #|Γ| = #|Γ'|
    on_contexts P Γ Γ'.
  Proof.
    intros. eapply on_contexts_app_inv in X; intuition auto.
  Qed.

  Lemma on_contexts_mapi P Γ Δ f g :
    All2_fold (on_decls
      (fun Γ Γ' t t'
        P (mapi_context f Γ) (mapi_context g Γ') (f #|Γ| t) (g #|Γ'| t'))) Γ Δ
    on_contexts P (mapi_context f Γ) (mapi_context g Δ).
  Proof.
    induction 1; rewrite /=; constructor; auto.
    depelim p; constructor; auto.
  Qed.

  Lemma on_contexts_mapi_inv P Γ Δ f g :
    on_contexts P (mapi_context f Γ) (mapi_context g Δ)
    on_contexts (fun Γ Γ' t t'
        P (mapi_context f Γ) (mapi_context g Γ') (f #|Γ| t) (g #|Γ'| t')) Γ Δ.
  Proof.
    induction Γ in Δ |- *; destruct Δ; intros h; depelim h.
    - constructor.
    - constructor; auto.
      destruct a as [na [b|] ty], c as [na' [b'|] ty']; cbn in × ⇒ //;
      depelim a0; constructor; auto.
  Qed.

End All2_fold.

Section ParallelReduction.
  Context (Σ : global_env).

  Definition pred_atom t :=
    match t with
    | tVar _
    | tSort _
    | tInd _ _
    | tConstruct _ _ _true
    
    | _false
    end.

  Reserved Notation "'pred1_ctx'" (at level 8).
  Reserved Notation "'pred1_ctx_over' Γ Γ'" (at level 200, Γ, Γ' at level 9).

  Inductive pred1 (Γ Γ' : context) : term term Type :=
  
Reductions Beta
  | pred_beta na t0 t1 b0 b1 a0 a1 :
    pred1 Γ Γ' t0 t1
    pred1 (Γ ,, vass na t0) (Γ' ,, vass na t1) b0 b1 pred1 Γ Γ' a0 a1
    pred1 Γ Γ' (tApp (tLambda na t0 b0) a0) (subst10 a1 b1)

  
Let
  | pred_zeta na d0 d1 t0 t1 b0 b1 :
    pred1 Γ Γ' t0 t1
    pred1 Γ Γ' d0 d1 pred1 (Γ ,, vdef na d0 t0) (Γ' ,, vdef na d1 t1) b0 b1
    pred1 Γ Γ' (tLetIn na d0 t0 b0) (subst10 d1 b1)

  
Local variables
  | pred_rel_def_unfold i body :
    pred1_ctx Γ Γ'
    option_map decl_body (nth_error Γ' i) = Some (Some body)
    pred1 Γ Γ' (tRel i) (lift0 (S i) body)

  | pred_rel_refl i :
    pred1_ctx Γ Γ'
    pred1 Γ Γ' (tRel i) (tRel i)

  
Case
Fix unfolding, with guard
CoFix-case unfolding
CoFix-proj unfolding
Constant unfolding
Proj
Congruences
  | pred_abs na M M' N N' :
    pred1 Γ Γ' M M'
    pred1 (Γ ,, vass na M) (Γ' ,, vass na M') N N'
    pred1 Γ Γ' (tLambda na M N) (tLambda na M' N')

  | pred_app M0 M1 N0 N1 :
    pred1 Γ Γ' M0 M1
    pred1 Γ Γ' N0 N1
    pred1 Γ Γ' (tApp M0 N0) (tApp M1 N1)

  | pred_letin na d0 d1 t0 t1 b0 b1 :
    pred1 Γ Γ' d0 d1 pred1 Γ Γ' t0 t1 pred1 (Γ ,, vdef na d0 t0) (Γ' ,, vdef na d1 t1) b0 b1
    pred1 Γ Γ' (tLetIn na d0 t0 b0) (tLetIn na d1 t1 b1)

  | pred_case ci p0 p1 c0 c1 brs0 brs1 :
    pred1_ctx Γ Γ'
    All2 (pred1 Γ Γ') p0.(pparams) p1.(pparams)
    p0.(puinst) = p1.(puinst)
    p0.(pcontext) = p1.(pcontext)
    pred1_ctx_over Γ Γ' (PCUICCases.inst_case_predicate_context p0) (PCUICCases.inst_case_predicate_context p1)
    pred1 (Γ ,,, inst_case_context p0.(pparams) p0.(puinst) p0.(pcontext))
      (Γ' ,,, inst_case_context p1.(pparams) p1.(puinst) p1.(pcontext)) p0.(preturn) p1.(preturn)
    All2 (fun br br'
      pred1_ctx_over Γ Γ' (inst_case_branch_context p0 br) (inst_case_branch_context p1 br') ×
      on_Trel_eq
        (pred1 (Γ ,,, inst_case_branch_context p0 br) (Γ' ,,, inst_case_branch_context p1 br'))
        bbody bcontext br br') brs0 brs1
    pred1 Γ Γ' c0 c1
    pred1 Γ Γ' (tCase ci p0 c0 brs0) (tCase ci p1 c1 brs1)

  | pred_proj_congr p c c' :
    pred1 Γ Γ' c c'
    pred1 Γ Γ' (tProj p c) (tProj p c')

  | pred_fix_congr mfix0 mfix1 idx :
    pred1_ctx Γ Γ'
    pred1_ctx_over Γ Γ' (fix_context mfix0) (fix_context mfix1)
    All2_prop2_eq Γ Γ' (Γ ,,, fix_context mfix0) (Γ' ,,, fix_context mfix1)
                  dtype dbody (fun x(dname x, rarg x)) pred1 mfix0 mfix1
    pred1 Γ Γ' (tFix mfix0 idx) (tFix mfix1 idx)

  | pred_cofix_congr mfix0 mfix1 idx :
    pred1_ctx Γ Γ'
    pred1_ctx_over Γ Γ' (fix_context mfix0) (fix_context mfix1)
    All2_prop2_eq Γ Γ' (Γ ,,, fix_context mfix0) (Γ' ,,, fix_context mfix1)
                  dtype dbody (fun x(dname x, rarg x)) pred1 mfix0 mfix1
    pred1 Γ Γ' (tCoFix mfix0 idx) (tCoFix mfix1 idx)

  | pred_prod na M0 M1 N0 N1 :
    pred1 Γ Γ' M0 M1
    pred1 (Γ ,, vass na M0) (Γ' ,, vass na M1) N0 N1
    pred1 Γ Γ' (tProd na M0 N0) (tProd na M1 N1)

  | evar_pred ev l l' :
    pred1_ctx Γ Γ'
    All2 (pred1 Γ Γ') l l' pred1 Γ Γ' (tEvar ev l) (tEvar ev l')

  | pred_atom_refl t :
    pred1_ctx Γ Γ'
    pred_atom t
    pred1 Γ Γ' t t

  where "'pred1_ctx'" := (All2_fold (on_decls pred1))
  and "'pred1_ctx_over' Γ Γ'" := (All2_fold (on_decls (on_decls_over pred1 Γ Γ'))).

  Derive Signature for pred1.

  Ltac my_rename_hyp h th :=
    match th with
    | pred1_ctx _ _ ?Gfresh "pred" G
    | nat boolfresh "P"
    | nat natfresh "f"
    | _PCUICWeakeningEnv.my_rename_hyp h th
    | _PCUICTyping.my_rename_hyp h th
    end.

  Ltac rename_hyp h ht ::= my_rename_hyp h ht.

  Definition extendP {P Q: context context term term Type}
             (aux : Γ Γ' t t', P Γ Γ' t t' Q Γ Γ' t t') :
    ( Γ Γ' t t', P Γ Γ' t t' (P Γ Γ' t t' × Q Γ Γ' t t')).
  Proof.
    intros. split. apply X. apply aux. apply X.
  Defined.

  Definition extend_over {P Q: context context term term Type}
             (aux : Γ Γ' t t', P Γ Γ' t t' Q Γ Γ' t t') Γ Γ' :
    ( Δ Δ' t t', P (Γ ,,, Δ) (Γ' ,,, Δ') t t' Q (Γ ,,, Δ) (Γ' ,,, Δ') t t').
  Proof.
    intros. apply aux. apply X.
  Defined.

  Lemma pred1_ind_all_ctx :
     (P : (Γ Γ' : context) (t t0 : term), Type)
           (Pctx : (Γ Γ' : context), Type)
           (Pctxover : (Γ Γ' Δ Δ' : context), Type),
      let P' Γ Γ' x y := ((pred1 Γ Γ' x y) × P Γ Γ' x y)%type in
      ( Γ Γ', pred1_ctx Γ Γ' on_contexts P Γ Γ' Pctx Γ Γ')
      ( Γ Γ' Δ Δ', pred1_ctx Γ Γ' on_contexts P Γ Γ'
        Pctx Γ Γ'
        pred1_ctx_over Γ Γ' Δ Δ'
        on_contexts_over P Γ Γ' Δ Δ'
        Pctxover Γ Γ' Δ Δ')
      ( (Γ Γ' : context) (na : aname) (t0 t1 b0 b1 a0 a1 : term),
          pred1 (Γ ,, vass na t0) (Γ' ,, vass na t1) b0 b1 P (Γ ,, vass na t0) (Γ' ,, vass na t1) b0 b1
          pred1 Γ Γ' t0 t1 P Γ Γ' t0 t1
          pred1 Γ Γ' a0 a1 P Γ Γ' a0 a1 P Γ Γ' (tApp (tLambda na t0 b0) a0) (b1 {0 := a1}))
      ( (Γ Γ' : context) (na : aname) (d0 d1 t0 t1 b0 b1 : term),
          pred1 Γ Γ' t0 t1 P Γ Γ' t0 t1
          pred1 Γ Γ' d0 d1 P Γ Γ' d0 d1
          pred1 (Γ ,, vdef na d0 t0) (Γ' ,, vdef na d1 t1) b0 b1
          P (Γ ,, vdef na d0 t0) (Γ' ,, vdef na d1 t1) b0 b1 P Γ Γ' (tLetIn na d0 t0 b0) (b1 {0 := d1}))
      ( (Γ Γ' : context) (i : nat) (body : term),
          pred1_ctx Γ Γ'
          Pctx Γ Γ'
          option_map decl_body (nth_error Γ' i) = Some (Some body)
          P Γ Γ' (tRel i) (lift0 (S i) body))
      ( (Γ Γ' : context) (i : nat),
          pred1_ctx Γ Γ'
          Pctx Γ Γ'
          P Γ Γ' (tRel i) (tRel i))
      ( Γ Γ' ci c u args0 args1 p0 pparams1 brs0 brs1 br,
          pred1_ctx Γ Γ'
          Pctx Γ Γ'
          All2 (P' Γ Γ') args0 args1
          All2 (P' Γ Γ') p0.(pparams) pparams1
          All2 (fun br br'
            Pctxover Γ Γ' (inst_case_branch_context p0 br)
              (inst_case_context pparams1 p0.(puinst) br'.(bcontext)) ×
            on_Trel_eq
              (P' (Γ ,,, inst_case_branch_context p0 br)
                  (Γ' ,,, inst_case_context pparams1 p0.(puinst) br'.(bcontext)))
              bbody bcontext br br') brs0 brs1
          nth_error brs1 c = Some br
          #|args1| = (ci.(ci_npar) + context_assumptions br.(bcontext))%nat
          P Γ Γ' (tCase ci p0 (mkApps (tConstruct ci.(ci_ind) c u) args0) brs0)
                (iota_red ci.(ci_npar) (set_pparams p0 pparams1) args1 br))

      ( (Γ Γ' : context) (mfix0 mfix1 : mfixpoint term) (idx : nat) (args0 args1 : list term) (narg : nat) (fn : term),
          pred1_ctx Γ Γ'
          Pctx Γ Γ'
          pred1_ctx_over Γ Γ' (fix_context mfix0) (fix_context mfix1)
          Pctxover Γ Γ' (fix_context mfix0) (fix_context mfix1)
          All2_prop2_eq Γ Γ' (Γ ,,, fix_context mfix0) (Γ' ,,, fix_context mfix1) dtype dbody
                        (fun x(dname x, rarg x)) P' mfix0 mfix1
          unfold_fix mfix1 idx = Some (narg, fn)
          is_constructor narg args0 = true
          All2 (P' Γ Γ') args0 args1
          P Γ Γ' (mkApps (tFix mfix0 idx) args0) (mkApps fn args1))

      ( (Γ Γ' : context) ci p0 p1 mfix0 mfix1 idx args0 args1 narg fn brs0 brs1,
          pred1_ctx Γ Γ'
          Pctx Γ Γ'
          pred1_ctx_over Γ Γ' (fix_context mfix0) (fix_context mfix1)
          Pctxover Γ Γ' (fix_context mfix0) (fix_context mfix1)
          All2_prop2_eq Γ Γ' (Γ ,,, fix_context mfix0) (Γ' ,,, fix_context mfix1)
                        dtype dbody (fun x(dname x, rarg x)) P' mfix0 mfix1
          unfold_cofix mfix1 idx = Some (narg, fn)
          All2 (P' Γ Γ') args0 args1
          All2 (P' Γ Γ') p0.(pparams) p1.(pparams)
          p0.(puinst) = p1.(puinst)
          p0.(pcontext) = p1.(pcontext)
          Pctxover Γ Γ' (PCUICCases.inst_case_predicate_context p0) (PCUICCases.inst_case_predicate_context p1)
          pred1 (Γ ,,, inst_case_context p0.(pparams) p0.(puinst) p0.(pcontext))
            (Γ' ,,, inst_case_context p1.(pparams) p1.(puinst) p1.(pcontext)) p0.(preturn) p1.(preturn)
          P (Γ ,,, inst_case_context p0.(pparams) p0.(puinst) p0.(pcontext))
            (Γ' ,,, inst_case_context p1.(pparams) p1.(puinst) p1.(pcontext)) p0.(preturn) p1.(preturn)
          All2 (fun br br'
            Pctxover Γ Γ' (inst_case_branch_context p0 br) (inst_case_branch_context p1 br') ×
              on_Trel_eq
                (P' (Γ ,,, inst_case_branch_context p0 br) (Γ' ,,, inst_case_branch_context p1 br'))
                  bbody bcontext br br') brs0 brs1
          P Γ Γ' (tCase ci p0 (mkApps (tCoFix mfix0 idx) args0) brs0)
                (tCase ci p1 (mkApps fn args1) brs1))

      ( (Γ Γ' : context) (p : projection) (mfix0 mfix1 : mfixpoint term)
         (idx : nat) (args0 args1 : list term)
         (narg : nat) (fn : term),
          pred1_ctx Γ Γ'
          Pctx Γ Γ'
          pred1_ctx_over Γ Γ' (fix_context mfix0) (fix_context mfix1)
          Pctxover Γ Γ' (fix_context mfix0) (fix_context mfix1)
          All2_prop2_eq Γ Γ' (Γ ,,, fix_context mfix0) (Γ' ,,, fix_context mfix1) dtype dbody
                        (fun x(dname x, rarg x)) P' mfix0 mfix1
          unfold_cofix mfix1 idx = Some (narg, fn)
          All2 (P' Γ Γ') args0 args1
          P Γ Γ' (tProj p (mkApps (tCoFix mfix0 idx) args0)) (tProj p (mkApps fn args1)))
      ( (Γ Γ' : context) c (decl : constant_body) (body : term),
          pred1_ctx Γ Γ'
          Pctx Γ Γ'
          declared_constant Σ c decl
           u : Instance.t, cst_body decl = Some body
                                        P Γ Γ' (tConst c u) (subst_instance u body))
      ( (Γ Γ' : context) c (u : Instance.t),
          pred1_ctx Γ Γ'
          Pctx Γ Γ'
          P Γ Γ' (tConst c u) (tConst c u))
      ( (Γ Γ' : context) p (u : Instance.t)
              (args0 args1 : list term) (arg1 : term),
          pred1_ctx Γ Γ'
          Pctx Γ Γ'
          All2 (pred1 Γ Γ') args0 args1
          All2 (P Γ Γ') args0 args1
          nth_error args1 (p.(proj_npars) + p.(proj_arg)) = Some arg1
          P Γ Γ' (tProj p (mkApps (tConstruct p.(proj_ind) 0 u) args0)) arg1)
      ( (Γ Γ' : context) (na : aname) (M M' N N' : term),
          pred1 Γ Γ' M M'
          P Γ Γ' M M' pred1 (Γ,, vass na M) (Γ' ,, vass na M') N N'
          P (Γ,, vass na M) (Γ' ,, vass na M') N N' P Γ Γ' (tLambda na M N) (tLambda na M' N'))
      ( (Γ Γ' : context) (M0 M1 N0 N1 : term),
          pred1 Γ Γ' M0 M1 P Γ Γ' M0 M1 pred1 Γ Γ' N0 N1
          P Γ Γ' N0 N1 P Γ Γ' (tApp M0 N0) (tApp M1 N1))
      ( (Γ Γ' : context) (na : aname) (d0 d1 t0 t1 b0 b1 : term),
          pred1 Γ Γ' d0 d1
          P Γ Γ' d0 d1
          pred1 Γ Γ' t0 t1
          P Γ Γ' t0 t1
          pred1 (Γ,, vdef na d0 t0) (Γ',,vdef na d1 t1) b0 b1
          P (Γ,, vdef na d0 t0) (Γ',,vdef na d1 t1) b0 b1 P Γ Γ' (tLetIn na d0 t0 b0) (tLetIn na d1 t1 b1))
      
      ( (Γ Γ' : context) ci p0 p1 c0 c1 brs0 brs1,
          pred1_ctx Γ Γ'
          Pctx Γ Γ'
          All2 (P' Γ Γ') p0.(pparams) p1.(pparams)
          p0.(puinst) = p1.(puinst)
          p0.(pcontext) = p1.(pcontext)
          Pctxover Γ Γ' (PCUICCases.inst_case_predicate_context p0) (PCUICCases.inst_case_predicate_context p1)
          pred1 (Γ ,,, inst_case_context p0.(pparams) p0.(puinst) p0.(pcontext))
            (Γ' ,,, inst_case_context p1.(pparams) p1.(puinst) p1.(pcontext)) p0.(preturn) p1.(preturn)
          P (Γ ,,, inst_case_context p0.(pparams) p0.(puinst) p0.(pcontext))
            (Γ' ,,, inst_case_context p1.(pparams) p1.(puinst) p1.(pcontext)) p0.(preturn) p1.(preturn)
          All2 (fun br br'
            Pctxover Γ Γ' (inst_case_branch_context p0 br) (inst_case_branch_context p1 br') ×
            on_Trel_eq
              (P' (Γ ,,, inst_case_branch_context p0 br) (Γ' ,,, inst_case_branch_context p1 br'))
                bbody bcontext br br') brs0 brs1
          pred1 Γ Γ' c0 c1
          P Γ Γ' c0 c1
          P Γ Γ' (tCase ci p0 c0 brs0) (tCase ci p1 c1 brs1))

      ( (Γ Γ' : context) (p : projection) (c c' : term), pred1 Γ Γ' c c' P Γ Γ' c c' P Γ Γ' (tProj p c) (tProj p c'))

      ( (Γ Γ' : context) (mfix0 : mfixpoint term) (mfix1 : list (def term)) (idx : nat),
          pred1_ctx Γ Γ'
          Pctx Γ Γ'
          pred1_ctx_over Γ Γ' (fix_context mfix0) (fix_context mfix1)
          Pctxover Γ Γ' (fix_context mfix0) (fix_context mfix1)
          All2_prop2_eq Γ Γ' (Γ ,,, fix_context mfix0) (Γ' ,,, fix_context mfix1)
                        dtype dbody (fun x(dname x, rarg x)) P' mfix0 mfix1
          P Γ Γ' (tFix mfix0 idx) (tFix mfix1 idx))

      ( (Γ Γ' : context) (mfix0 : mfixpoint term) (mfix1 : list (def term)) (idx : nat),
          pred1_ctx Γ Γ'
          Pctx Γ Γ'
          pred1_ctx_over Γ Γ' (fix_context mfix0) (fix_context mfix1)
          Pctxover Γ Γ' (fix_context mfix0) (fix_context mfix1)
          All2_prop2_eq Γ Γ' (Γ ,,, fix_context mfix0) (Γ' ,,, fix_context mfix1) dtype dbody (fun x(dname x, rarg x)) P' mfix0 mfix1
          P Γ Γ' (tCoFix mfix0 idx) (tCoFix mfix1 idx))
      ( (Γ Γ' : context) (na : aname) (M0 M1 N0 N1 : term),
          pred1 Γ Γ' M0 M1
          P Γ Γ' M0 M1 pred1 (Γ,, vass na M0) (Γ' ,, vass na M1) N0 N1
          P (Γ,, vass na M0) (Γ' ,, vass na M1) N0 N1 P Γ Γ' (tProd na M0 N0) (tProd na M1 N1))
      ( (Γ Γ' : context) (ev : nat) (l l' : list term),
          pred1_ctx Γ Γ'
          Pctx Γ Γ'
          All2 (P' Γ Γ') l l' P Γ Γ' (tEvar ev l) (tEvar ev l'))
      ( (Γ Γ' : context) (t : term),
          pred1_ctx Γ Γ'
          Pctx Γ Γ'
          pred_atom t P Γ Γ' t t)
      ( (Γ Γ' : context) (t t0 : term), pred1 Γ Γ' t t0 P Γ Γ' t t0) ×
      ( Γ Γ' Δ Δ', pred1_ctx Γ Γ' pred1_ctx_over Γ Γ' Δ Δ' Pctxover Γ Γ' Δ Δ').
  Proof using Σ.
    intros P Pctx Pctxover P' Hctx Hctxover. intros.
    assert ( (Γ Γ' : context) (t t0 : term), pred1 Γ Γ' t t0 P Γ Γ' t t0).
    intros.
    rename X20 into pr. revert Γ Γ' t t0 pr.
    fix aux 5. intros Γ Γ' t t'.
    move aux at top.
    destruct 1; match goal with
                | |- P _ _ (tFix _ _) (tFix _ _) ⇒ idtac
                | |- P _ _ (tCoFix _ _) (tCoFix _ _) ⇒ idtac
                | |- P _ _ (mkApps (tFix _ _) _) _idtac
                | |- P _ _ (tCase _ _ (mkApps (tCoFix _ _) _) _) _idtac
                | |- P _ _ (tProj _ (mkApps (tCoFix _ _) _)) _idtac
                | |- P _ _ (tRel _) _idtac
                | |- P _ _ (tConst _ _) _idtac
                | |- P _ _ (tCase _ _ ?c _) (tCase _ _ ?c _) ⇒ idtac
                | H : _ |- _eapply H; eauto
                end.
    - simpl. apply X1; auto.
      clear X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 X14 X15 X16 X17 X18 X19.
      apply Hctx.
      apply (on_contexts_impl a). intros. eapply X1.
      apply (on_contexts_impl a). intros. eapply (aux _ _ _ _ X1).
    - simpl. apply X2; auto.
      apply Hctx, (on_contexts_impl a). exact a. intros. apply (aux _ _ _ _ X20).
    - apply Hctx, (on_contexts_impl a). exact a. intros. apply (aux _ _ _ _ X20).
    - eapply (All2_All2_prop (P:=pred1) (Q:=P') a0 ((extendP aux) Γ Γ')).
    - eapply (All2_All2_prop a1 (extendP aux Γ Γ')).
    - eapply (All2_branch_prop
        (P:=fun Γ Γ' br br'
        (pred1_ctx_over Γ Γ') (inst_case_branch_context p0 br)
          (inst_case_context params' (puinst p0) (bcontext br')) ×
        (pred1 (Γ,,, inst_case_branch_context p0 br)
           (Γ',,, inst_case_context params' (puinst p0) (bcontext br))
           (bbody br) (bbody br') × bcontext br = bcontext br'))
        (Q:=fun Γ Γ' br0 br'
        Pctxover Γ Γ' (inst_case_branch_context p0 br0)
     (inst_case_context params' (puinst p0) (bcontext br')) ×
   (P' (Γ,,, inst_case_branch_context p0 br0)
      (Γ',,, inst_case_context params' (puinst p0) (bcontext br'))
      (bbody br0) (bbody br') × bcontext br0 = bcontext br')) a2).
      intros x y [? []]. split; [|split]; auto.
      × apply Hctxover ⇒ //.
        apply (on_contexts_impl a aux).
        apply (Hctx _ _ a), (on_contexts_impl a aux).
        apply (on_contexts_impl a3 (extend_over aux Γ Γ')).
      × apply (extendP aux _ _). rewrite -e1. exact p.
    - eapply X4; eauto.
      × apply (Hctx _ _ a), (on_contexts_impl a aux).
      × apply (Hctxover _ _ _ _ a (on_contexts_impl a aux)
          (Hctx _ _ a (on_contexts_impl a aux)) a0 (on_contexts_impl a0 (extend_over aux Γ Γ'))).
      × eapply (All2_All2_prop2_eq (Q:=P') (f:=dtype) (g:=dbody) a1 (extendP aux)).
      × eapply (All2_All2_prop (P:=pred1) (Q:=P') a2 (extendP aux Γ Γ')).
    - eapply X5; eauto.
      × apply Hctx, (on_contexts_impl a) ⇒ //.
      × apply (Hctxover _ _ _ _ a (on_contexts_impl a aux)
        (Hctx _ _ a (on_contexts_impl a aux)) a0 (on_contexts_impl a0 (extend_over aux Γ Γ'))).
      × eapply (All2_All2_prop2_eq (Q:=P') (f:=dtype) (g:=dbody) a1 (extendP aux)).
      × eapply (All2_All2_prop (P:=pred1) (Q:=P') a2 (extendP aux Γ Γ')).
      × eapply (All2_All2_prop (P:=pred1) (Q:=P') a3 (extendP aux Γ Γ')).
      × apply (Hctxover _ _ _ _ a (on_contexts_impl a aux)
        (Hctx _ _ a (on_contexts_impl a aux))
        a4 (on_contexts_impl a4 (extend_over aux Γ Γ'))).
      × eapply (All2_branch_prop
          (P:=fun Γ Γ' br br'
          (pred1_ctx_over Γ Γ') (inst_case_branch_context p0 br)
            (inst_case_branch_context p1 br') ×
          (pred1 (Γ,,, inst_case_branch_context p0 br)
            (Γ',,, inst_case_branch_context p1 br')
            (bbody br) (bbody br') × bcontext br = bcontext br'))
          (Q:=fun Γ Γ' br0 br'
          Pctxover Γ Γ' (inst_case_branch_context p0 br0)
          (inst_case_branch_context p1 br') ×
        (P' (Γ,,, inst_case_branch_context p0 br0)
            (Γ',,, inst_case_branch_context p1 br')
            (bbody br0) (bbody br') × bcontext br0 = bcontext br')) a5).
        intros x y [? []].
        split; auto. 2:split ⇒ //.
        + apply (Hctxover _ _ _ _ a (on_contexts_impl a aux)
            (Hctx _ _ a (on_contexts_impl a aux)) a6 (on_contexts_impl a6 (extend_over aux Γ Γ'))).
        + apply (extendP aux _ _). exact p.
    - eapply X6; eauto.
      × apply (Hctx _ _ a), (on_contexts_impl a aux).
      × apply (Hctxover _ _ _ _ a (on_contexts_impl a aux)
          (Hctx _ _ a (on_contexts_impl a aux)) a0 (on_contexts_impl a0 (extend_over aux Γ Γ'))).
      × eapply (All2_All2_prop2_eq (Q:=P') (f:=dtype) (g:=dbody) a1 (extendP aux)).
      × eapply (All2_All2_prop (P:=pred1) (Q:=P') a2 (extendP aux Γ Γ')).
    - eapply X7; eauto.
      apply (Hctx _ _ a), (on_contexts_impl a aux).
    - eapply X8; eauto.
      apply (Hctx _ _ a), (on_contexts_impl a aux).
    - apply (Hctx _ _ a), (on_contexts_impl a aux).
    - eapply (All2_All2_prop (P:=pred1) (Q:=P) a0). intros. apply (aux _ _ _ _ X20).
    - apply (Hctx _ _ a), (on_contexts_impl a aux).
    - apply (All2_All2_prop (P:=pred1) (Q:=P') a0 (extendP aux _ _)).
    - apply (Hctxover _ _ _ _ a (on_contexts_impl a aux)
        (Hctx _ _ a (on_contexts_impl a aux)) a1 (on_contexts_impl a1 (extend_over aux Γ Γ'))).
    - eapply (All2_branch_prop
        (P:=fun Γ Γ' br br'
        (pred1_ctx_over Γ Γ') (inst_case_branch_context p0 br)
          (inst_case_branch_context p1 br') ×
        (pred1 (Γ,,, inst_case_branch_context p0 br)
          (Γ',,, inst_case_branch_context p1 br')
          (bbody br) (bbody br') × bcontext br = bcontext br'))
        (Q:=fun Γ Γ' br0 br'
        Pctxover Γ Γ' (inst_case_branch_context p0 br0)
        (inst_case_branch_context p1 br') ×
      (P' (Γ,,, inst_case_branch_context p0 br0)
          (Γ',,, inst_case_branch_context p1 br')
          (bbody br0) (bbody br') × bcontext br0 = bcontext br')) a2).
      intros x y [? []].
      split; auto. 2:split ⇒ //.
      + apply (Hctxover _ _ _ _ a (on_contexts_impl a aux)
          (Hctx _ _ a (on_contexts_impl a aux)) a3 (on_contexts_impl a3 (extend_over aux Γ Γ'))).
      + apply (extendP aux _ _). exact p.
    - eapply X15 ⇒ //.
      × eapply (Hctx _ _ a), (on_contexts_impl a aux).
      × apply (Hctxover _ _ _ _ a (on_contexts_impl a aux)
         (Hctx _ _ a (on_contexts_impl a aux)) a0 (on_contexts_impl a0 (extend_over aux Γ Γ'))).
      × eapply (All2_All2_prop2_eq (Q:=P') (f:=dtype) (g:=dbody) a1 (extendP aux)).
    - eapply X16; tas.
      × eapply (Hctx _ _ a), (on_contexts_impl a aux).
      × apply (Hctxover _ _ _ _ a (on_contexts_impl a aux)
        (Hctx _ _ a (on_contexts_impl a aux)) a0 (on_contexts_impl a0 (extend_over aux Γ Γ'))).
      × eapply (All2_All2_prop2_eq (Q:=P') (f:=dtype) (g:=dbody) a1 (extendP aux)).
    - eapply (Hctx _ _ a), (on_contexts_impl a aux).
    - eapply (All2_All2_prop (P:=pred1) (Q:=P') a0 (extendP aux Γ Γ')).
    - eapply (Hctx _ _ a), (on_contexts_impl a aux).
    - split ⇒ //.
      intros.
      eapply Hctxover; eauto.
      { eapply (on_contexts_impl X21 X20). }
      eapply Hctx; eauto.
      { eapply (on_contexts_impl X21 X20). }
      eapply (on_contexts_impl X22 (extend_over X20 Γ Γ')).
  Defined.

  Lemma pred1_pred1_ctx {Γ Δ t u} : pred1 Γ Δ t u pred1_ctx Γ Δ.
  Proof using.
    intros H; revert Γ Δ t u H.
    refine (fst (pred1_ind_all_ctx _ (fun Γ Γ'pred1_ctx Γ Γ')
      (fun Γ Γ' Δ Δ'True)
      _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _)); intros ×.
    all:try intros **; rename_all_hyps;
      try solve [specialize (forall_Γ _ X3); eauto]; eauto;
        try solve [eexists; split; constructor; eauto].
  Qed.

  Lemma onctx_rel_pred1_refl Γ Δ :
     Γ',
    pred1_ctx Γ Γ'
    onctx_rel
    (fun (Γ : context) (t : term) ⇒
       Γ' : context, pred1_ctx Γ Γ' pred1 Γ Γ' t t) Γ Δ
    pred1_ctx_over Γ Γ' Δ Δ.
  Proof using.
    intros Γ' pred onc.
    induction onc; simpl; constructor; auto.
    constructor.
    eapply t0.
    apply on_contexts_app ⇒ //.
    destruct t1.
    constructor; [eapply p|eapply p0];
    apply on_contexts_app ⇒ //.
  Qed.

  Lemma onctx_rel_pred1_refl' Γ Δ :
     Γ',
    pred1_ctx Γ Γ'
    onctx_rel
    (fun (Γ : context) (t : term) ⇒
       Γ' : context, pred1_ctx Γ Γ' pred1 Γ Γ' t t) Γ Δ
    pred1_ctx_over Γ Γ' Δ Δ.
  Proof using.
    intros Γ' pred onc.
    induction onc; simpl; constructor; auto.
    constructor.
    eapply t0.
    apply on_contexts_app ⇒ //.
    destruct t1.
    constructor; [eapply p|eapply p0];
    apply on_contexts_app ⇒ //.
  Qed.

  Hint Constructors All_decls : pcuic.

  Lemma pred1_refl_gen Γ Γ' t : pred1_ctx Γ Γ' pred1 Γ Γ' t t.
  Proof using.
    revert Γ'.
    revert Γ t.
    apply: PCUICDepth.term_forall_ctx_list_ind;
    intros;
      try solve [(apply pred_atom; reflexivity) || constructor; auto];
      try solve [try red in X; constructor; unfold All2_prop2_eq, All2_prop2, on_Trel in *; solve_all];
      intros.
    - constructor; eauto. eapply X0.
      constructor; try red; eauto with pcuic.
    - constructor; eauto. eapply X0.
      constructor; try red; eauto with pcuic.
    - constructor; eauto. eapply X1.
      constructor; try red; eauto with pcuic.
    - red in X, X1; econstructor; solve_all.
      × eapply onctx_rel_pred1_refl ⇒ //.
      × eapply b0.
        eapply on_contexts_app ⇒ //.
        eapply onctx_rel_pred1_refl ⇒ //.
      × eapply All_All2; tea; solve_all.
        + eapply onctx_rel_pred1_refl ⇒ //.
        + eapply b.
          now eapply on_contexts_app ⇒ //; eapply onctx_rel_pred1_refl.
    - constructor; auto.
      apply onctx_rel_pred1_refl ⇒ //.
      unfold All2_prop_eq, on_Trel in ×.
      eapply All_All2; eauto. simpl; intros. solve_all.
      eapply a; tas.
      eapply b. eapply on_contexts_app; auto.
      now eapply onctx_rel_pred1_refl.
    - constructor; auto.
      apply onctx_rel_pred1_refl ⇒ //.
      unfold All2_prop_eq, on_Trel in ×.
      eapply All_All2; eauto. simpl; intros. solve_all.
      eapply a; tas.
      eapply b. eapply on_contexts_app; auto.
      now eapply onctx_rel_pred1_refl.
  Qed.

  Lemma pred1_ctx_refl Γ : pred1_ctx Γ Γ.
  Proof using.
    induction Γ. constructor.
    destruct a as [na [b|] ty]; constructor; try red; simpl; auto with pcuic;
    constructor; now apply pred1_refl_gen.
  Qed.
  Hint Resolve pred1_ctx_refl : pcuic.

  Lemma pred1_refl Γ t : pred1 Γ Γ t t.
  Proof using Type×. apply pred1_refl_gen, pred1_ctx_refl. Qed.

  Lemma pred1_ctx_over_refl Γ Δ : All2_fold (on_decls (on_decls_over pred1 Γ Γ)) Δ Δ.
  Proof using.
    induction Δ as [|[na [b|] ty] Δ]; constructor; auto.
    all:constructor; apply pred1_refl.
  Qed.

End ParallelReduction.

#[global]
Hint Constructors pred1 : pcuic.
#[global]
Hint Unfold All2_prop2_eq All2_prop2 on_rel on_Trel snd on_snd : pcuic.
#[global]
Hint Resolve All2_same: pcuic.
#[global]
Hint Constructors All2_fold : pcuic.
#[global]
Hint Resolve pred1_ctx_refl : pcuic.

Ltac pcuic_simplify :=
  simpl || split || rdest || red.

#[global]
Hint Extern 10 ⇒ progress pcuic_simplify : pcuic.

Notation pred1_ctx Σ Γ Γ' := (All2_fold (on_decls (pred1 Σ)) Γ Γ').
Notation pred1_ctx_over Σ Γ Γ' := (All2_fold (on_decls (on_decls_over (pred1 Σ) Γ Γ'))).

#[global]
Hint Extern 4 (pred1 _ _ _ ?t _) ⇒ tryif is_evar t then fail 1 else eapply pred1_refl_gen : pcuic.
#[global]
Hint Extern 4 (pred1 _ _ _ ?t _) ⇒ tryif is_evar t then fail 1 else eapply pred1_refl : pcuic.

#[global]
Hint Extern 20 (#|?X| = #|?Y|) ⇒
match goal with
  [ H : All2_fold _ ?X ?Y |- _ ] ⇒ apply (on_contexts_length H)
| [ H : All2_fold _ ?Y ?X |- _ ] ⇒ symmetry; apply (on_contexts_length H)
| [ H : on_contexts_over _ _ _ ?X ?Y |- _ ] ⇒ apply (on_contexts_length H)
| [ H : on_contexts_over _ _ _ ?Y ?X |- _ ] ⇒ symmetry; apply (on_contexts_length H)
end : pcuic.

#[global]
Hint Extern 4 (pred1_ctx ?Σ ?Γ ?Γ') ⇒
  match goal with
  | [ H : pred1_ctx Σ (Γ ,,, _) (Γ' ,,, _) |- _ ] ⇒ apply (on_contexts_app_inv_left H)
  | [ H : pred1 Σ Γ Γ' _ _ |- _ ] ⇒ apply (pred1_pred1_ctx _ H)
  end : pcuic.

Ltac pcuic := try repeat red; cbn in *; try solve [intuition auto; eauto with pcuic || ltac:(try (lia || congruence))].

Ltac my_rename_hyp h th :=
  match th with
  | pred1_ctx _ _ ?Gfresh "pred" G
  | nat boolfresh "P"
  | nat natfresh "f"
  | urenaming _ _ _ ?ffresh "u" f
  | _PCUICWeakeningEnv.my_rename_hyp h th
  | _PCUICTyping.my_rename_hyp h th
  end.

Ltac rename_hyp h ht ::= my_rename_hyp h ht.

Lemma on_contexts_over_refl {Σ Γ Δ Γ'} :
  pred1_ctx Σ Γ Δ on_contexts_over (pred1 Σ) Γ Δ Γ' Γ'.
Proof.
  intros X0.
  induction Γ'. constructor.
  pose proof IHΓ'. apply on_contexts_over_app in IHΓ'; auto.
  constructor; auto.
  destruct a as [na [b|] ty]; constructor; pcuic.
Qed.

#[global]
Hint Extern 4 (on_contexts_over _ _ _ ?X) ⇒
  tryif is_evar X then fail 1 else eapply on_contexts_over_refl : pcuic.

Ltac inv_on_free_vars ::=
  match goal with
  | [ H : is_true (on_free_vars ?P ?t) |- _ ] ⇒
    progress (cbn in H || rewriteon_free_vars_mkApps in H);
    (move/and5P: H ⇒ [] || move/and4P: H ⇒ [] || move/and3P: H ⇒ [] || move/andP: H ⇒ [] ||
      eapply forallb_All in H); intros
  end.

#[global]
Hint Resolve on_free_vars_fix_context : fvs.

Section ParallelWeakening.
  Context {cf : checker_flags}.

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

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

  Lemma lift_rename' n k : lift n k =1 rename (lift_renaming n k).
  Proof. intros t; apply lift_rename. Qed.

  Lemma lift_iota_red n k pars p args br :
    #|args| = (pars + context_assumptions br.(bcontext))%nat
    test_context_k closedn #|pparams p| (bcontext br)
    lift n k (iota_red pars p args br) =
    iota_red pars (map_predicate_k id (lift n) k p) (List.map (lift n k) args) (map_branch_k (lift n) id k br).
  Proof.
    intros hctx hctx'. rewrite !lift_rename'.
    rewrite rename_iota_red //; try (rewrite skipn_length; lia).
    f_equal; try setoid_rewrite <-lift_rename ⇒ //.
    unfold map_branch_k, rename_branch, map_branch_shift.
    f_equal.
    × rewrite /shiftf /rename_predicate /map_predicate_k /= /id.
      f_equal.
      now setoid_rewrite lift_rename'.
      setoid_rewrite shiftn_lift_renaming.
      now rewrite lift_rename'.
    × rewrite /rename_branch /PCUICSigmaCalculus.rename_branch /map_branch_k /= /id.
      f_equal. now rewrite lift_rename' shiftn_lift_renaming.
  Qed.

  Lemma mapi_context_lift n k ctx :
    mapi_context (shiftf (lift n) k) ctx = lift_context n k ctx.
  Proof.
    now rewrite mapi_context_fold.
  Qed.

  Lemma All_decls_map P (f g : term term) d d' :
    All_decls (fun x yP (f x) (g y)) d d'
    All_decls P (map_decl f d) (map_decl g d').
  Proof.
    intros []; constructor; auto.
  Qed.

  Lemma on_contexts_context_k P (f g : nat term term) ctx ctx' :
  All2_fold (fun Γ Γ' d d'P (map_decl (f #|Γ|) d) (map_decl (g #|Γ'|) d')) ctx ctx'
  All2 P (fold_context_k f ctx) (fold_context_k g ctx').
Proof.
  induction 1. constructor.
  rewrite !fold_context_k_snoc0. now constructor.
Qed.

  Hint Resolve urenaming_vass urenaming_vdef : pcuic.

  Lemma on_contexts_fold_context_k P (f g : nat term term) ctx ctx' :
    All2_fold (on_decls (fun Γ Γ' t t'P (fold_context_k f Γ) (fold_context_k g Γ')
    (f #|Γ| t) (g #|Γ'| t'))) ctx ctx'
    All2_fold (on_decls P) (fold_context_k f ctx) (fold_context_k g ctx').
  Proof.
    intros a. rewrite - !mapi_context_fold.
    eapply on_contexts_mapi.
    eapply (on_contexts_impl_ind a).
    intros par par' x y H.
    now rewrite !mapi_context_fold.
  Qed.

  Lemma on_contexts_rename_context Σ Δ Δ' Γ Γ' f :
    All2_fold
      (fun Γ Γ' : context
       All_decls
         (fun t t' : term
          on_decls_over (pred1 Σ) Δ Δ'
            (fold_context_k (fun i : natrename (shiftn i f)) Γ)
            (fold_context_k (fun i : natrename (shiftn i f)) Γ')
            (rename (shiftn #|Γ| f) t) (rename (shiftn #|Γ'| f) t'))) Γ Γ'
    pred1_ctx_over Σ Δ Δ' (rename_context f Γ) (rename_context f Γ').
  Proof.
    intros q.
    now eapply on_contexts_fold_context_k.
  Qed.

  Lemma All_decls_on_free_vars_impl P Q R d d' :
    All_decls P d d'
    on_free_vars_decl R d
    ( t t', on_free_vars R t P t t' Q t t')
    All_decls Q d d'.
  Proof.
    move⇒ [] /=; constructor; auto.
    eapply X; eauto with pcuic.
    now move/andP: H ⇒ /= [].
    now move/andP: H ⇒ /= [].
  Qed.

This not only proves that parallel reduction has renaming, it also ensures that it only looks at the variables actually used in the term/context. This lemma can later be used to show weakening but also verify that strenghtening is admissible for parallel reduction: i.e. the case of a renaming that is only defined on a subset of the variables of the context.

  Lemma pred1_rename {Σ} {wfΣ : wf Σ} :
    ( Γ Γ' u v, pred1 Σ Γ Γ' u v
     {P f Δ Δ'},
    pred1_ctx Σ Δ Δ'
    urenaming P Δ Γ f
    urenaming P Δ' Γ' f
    on_free_vars P u
    on_ctx_free_vars P Γ
    pred1 Σ Δ Δ' (rename f u) (rename f v)) ×
    ( (Γ Γ' : context) (Δ Δ' : context),
      pred1_ctx Σ Γ Γ'
      pred1_ctx_over Σ Γ Γ' Δ Δ'
       P f Δ0 Δ'0,
        urenaming P Δ0 Γ f
        urenaming P Δ'0 Γ' f
        pred1_ctx Σ Δ0 Δ'0
        on_ctx_free_vars P Γ
        on_free_vars_ctx P Δ
        pred1_ctx_over Σ Δ0 Δ'0 (rename_context f Δ) (rename_context f Δ')).
  Proof using cf.
    set (Pctx := fun (Γ Γ' : context) ⇒ pred1_ctx Σ Γ Γ').

    refine (pred1_ind_all_ctx Σ _ Pctx _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _); intros *; intros;
      subst Pctx;
    rename_all_hyps; try subst Γ Γ';
    lazymatch goal with
    | |- context [tCase _ _ _ _] ⇒ idtac
    | |- _simplify_IH_hyps
    end; cbn -[iota_red];
    match goal with
    |- context [iota_red _ _ _] ⇒ idtac
    | |- _autorewrite with lift
    end;
    try specialize (forall_P P f Δ Δ' uf uf0);
    try specialize (forall_P0 P f Δ Δ' uf uf0);
    try specialize (forall_P1 P f Δ Δ' uf uf0);
    try pose proof (on_contexts_length X0);
    try specialize (X0 _ _ eq_refl _ _ eq_refl heq_length _ _ ltac:(eauto));
    simpl; try solve [ econstructor; eauto; try apply All2_map;
                    unfold All2_prop_eq, All2_prop, on_Trel, id in *; solve_all];
    unfold All2_prop_eq, All2_prop, on_Trel, id in ×.
    all:try inv_on_free_vars.
    all:try solve [econstructor; eauto].
    12:{
      econstructor; eauto.
      eapply forall_P0; eauto with pcuic.
      repeat (econstructor; eauto).
    }
    15:{
      econstructor; eauto.
      rewrite !rename_fix_context. eapply forall_P; tea; eauto with fvs.
      red in X3 |- ×.
      eapply All2_All_mix_left in X3; tea.
      eapply All2_map.
      rewrite /= !rename_fix_context /= /on_Trel /=.
      rewrite /on_Trel /= in X3.
      pose proof (All2_length X3).
      eapply (All2_impl X3). intuition auto.
      move/andP: a ⇒ [] clty cldef.
      eapply b; tea.
      rewrite -H2.
      eapply b0; tea.
      × eapply on_contexts_app ⇒ //. eapply X2; tea; eauto with fvs.
      × relativize #|mfix0|; [eapply urenaming_context|]; tea; now len.
      × len; relativize #|mfix0|; [eapply urenaming_context|]; tea; now len.
      × move/andP: a ⇒ []. now len.
      × rewrite on_ctx_free_vars_concat H0 /=.
        rewrite on_free_vars_ctx_on_ctx_free_vars. now eapply on_free_vars_fix_context.
    }

    1:{ exact predΓ'. }
        
    - rename uf0 into uf'.
      rename H into onΓ; rename H0 into onΔ.
      eapply on_contexts_fold_context_k.
      induction X3.
      × constructor; auto.
      × move: onΔ.
        rewrite -on_free_vars_ctx_on_ctx_free_vars on_ctx_free_vars_snocS ⇒ /andP[] onΓ0 ond.
        rewrite on_free_vars_ctx_on_ctx_free_vars in onΓ0.
        depelim X2.
        do 2 forward IHX3 by auto.
        constructor; auto.
        eapply All_decls_on_free_vars_impl; tea.
        intros t t' ont IH.
        rewrite -(on_contexts_length IHX3).
        rewrite - !/(rename_context _ _).
        eapply IH; tea; auto with pcuic.
        + eapply on_contexts_app ⇒ //.
          eapply on_contexts_fold_context_k ⇒ //.
        + now eapply urenaming_context.
        + rewrite (on_contexts_length IHX3). now eapply urenaming_context.
        + now rewrite on_ctx_free_vars_concat onΓ on_free_vars_ctx_on_ctx_free_vars onΓ0.

    -
      move/andP: a ⇒ [] onty onbody.
      rewrite rename_subst10.
      econstructor; eauto.
      eapply (forall_P (PCUICOnFreeVars.shiftnP 1 P) (shiftn 1 f)); auto with pcuic.
      repeat (constructor; eauto).

    -
      rewrite rename_subst10.
      econstructor; eauto.
      eapply (forall_P1 (PCUICOnFreeVars.shiftnP 1 P) (shiftn 1 f)); eauto with pcuic.
      repeat (constructor; eauto).

    -
      rewrite lift0_rename /rshiftk.
      cbn in H0.
      epose proof (nth_error_pred1_ctx _ _ predΓ' heq_option_map) as [bod [hbod predbod]].
      destruct (nth_error Γ i) eqn:hnth ⇒ //. noconf hbod.
      destruct (nth_error Γ' i) eqn:hnth' ⇒ //.
      simpl in X0.
      unfold urenaming in uf, uf0.
      specialize uf0 with (1 := H0) (2 := hnth') as [decl' [nthΔ' [eqba [reneq onb]]]].
      specialize uf with (1 := H0) (2 := hnth) as [decl'' [nthΔ'' [eqba' [reneq' onb']]]].
      cbn in heq_option_map. noconf heq_option_map.
      rewrite H in onb. rewrite H3 in onb'; cbn in ×.
      destruct decl' as [? [?|] ?]; noconf onb; cbn in ×.
      destruct decl'' as [? [?|] ?]; noconf onb'; cbn in ×.
      rewrite rename_compose H4.
      replace (rename (fun mS (f i + m)) t) with (lift0 (S (f i)) t).
      2:{ rewrite lift0_rename //. }
      econstructor; eauto.
      rewrite nthΔ' /= //.

    -
      rewrite rename_mkApps. simpl.
      eapply forallb_All in p4.
      eapply All2_All_mix_left in X3; tea.
      rewrite rename_iota_red //.
      × rewrite skipn_length; lia.
      × eapply All2_nth_error_Some_right in X3 as [br' [nthbr [? []]]]; tea.
        move/andP: i ⇒ [] clbctx onfvs.
        destruct p5.
        rewrite -e.
        rewrite test_context_k_closed_on_free_vars_ctx in clbctx. len.
        rewrite -(All2_length X2).
        now rewrite closedn_ctx_on_free_vars.
      × move: p3; rewrite on_free_vars_mkApps /= ⇒ /forallb_All Hargs.
        eapply All2_All_mix_left in X1; tea.
        rewrite rename_predicate_set_pparams.
        econstructor; tea; try solve [solve_all].
        + erewrite nth_error_map, heq_nth_error ⇒ //.
        + simpl. eapply All2_map; solve_all.
        + eapply All2_map, (All2_impl X3).
          movex y [] /andP [] onctx onb [] IHctx [] [] Hbod IHbod eqc; cbn.
          simpl.
          rewrite -eqc.
          rewrite {2}/id.
          rewrite /PCUICSigmaCalculus.rename_branch /inst_case_branch_context /= /id.
          rewrite -rename_inst_case_context_wf //.
          rewrite -rename_inst_case_context_wf //.
          { now rewrite -(All2_length X2). }
          split.
          { rewrite -eqc in IHctx. eapply IHctx; tea.
            eapply on_free_vars_ctx_inst_case_context; tea ⇒ //. }
          split ⇒ //. eapply IHbod; tea.
          { eapply on_contexts_app ⇒ //. rewrite -eqc in IHctx. eapply IHctx; tea.
            eapply on_free_vars_ctx_inst_case_context; tea. reflexivity. }
          { relativize #|bcontext x|; [apply: urenaming_context|] ⇒ //.
            now rewrite inst_case_context_length. }
          { rewrite -eqc. relativize #|bcontext x|; [apply: urenaming_context|] ⇒ //.
            now rewrite inst_case_context_length. }
          { relativize #|bcontext x|; [erewrite on_ctx_free_vars_concat, H2|].
            2:{ now rewrite inst_case_context_length. }
            rewrite /=.
            rewrite on_free_vars_ctx_on_ctx_free_vars.
            eapply on_free_vars_ctx_inst_case_context; trea. }

    -
      rewrite 2!rename_mkApps. simpl. inv_on_free_vars.
      econstructor; tas.
      3:eapply rename_unfold_fix; tea.
      3:rewrite -is_constructor_rename; tea.
      + rewrite !rename_fix_context.
        eapply forall_P; tea.
        eapply on_free_vars_fix_context; solve_all.
      + red in X3 |- ×. pose proof (All2_length X3).
        eapply All2_All_mix_left in X3; tea.
        eapply All2_map ⇒ /=; rewrite /on_Trel /=.
        rewrite !rename_fix_context.
        eapply (All2_impl X3); solve_all.
        unfold on_Trel in *; cbn; solve_all.
        eapply b1; tea. now move/andP: a.
        rewrite -H0; eapply b0; tea.
        × eapply on_contexts_app ⇒ //. eapply X2; tea.
          eapply on_free_vars_fix_context. solve_all.
        × relativize #|mfix0|; [eapply urenaming_context|]; tea; now len.
        × len. relativize #|mfix0|; [eapply urenaming_context|]; tea; now len.
        × len. now move/andP: a.
        × rewrite on_ctx_free_vars_concat on_free_vars_ctx_on_ctx_free_vars H2.
          eapply on_free_vars_fix_context; solve_all.
      + solve_all.

    - rewrite 2!rename_mkApps. simpl. repeat inv_on_free_vars.
      eapply pred_cofix_case; tea.
      3:eapply rename_unfold_cofix; tea.
      all:try rewrite !rename_fix_context.
      + eapply forall_P; tea.
        eapply on_free_vars_fix_context; solve_all.
      + eapply All2_All_mix_left in X3; tea.
        eapply All2_map, (All2_impl X3); unfold on_Trel; cbn.
        movex y [] /andP[] onty onbod [] [] pty IHbty [] [] pbody IHpbody [=] eqna eqrarg.
        solve_all.
        rewrite -(All2_length X3).
        rewrite -(fix_context_length mfix0) in onbod ×.
        eapply IHpbody; tea.
        × eapply on_contexts_app ⇒ //. eapply X6; eauto.
          eapply on_free_vars_fix_context; solve_all.
        × now eapply urenaming_context.
        × relativize #|fix_context mfix0|; [eapply urenaming_context|]; len; trea.
          now rewrite (All2_length X3).
        × rewrite on_ctx_free_vars_concat H3 /= on_free_vars_ctx_on_ctx_free_vars.
          eapply on_free_vars_fix_context; solve_all.
      + solve_all.
      + cbn. solve_all.
      + cbn. rewrite /map_predicate_shift /PCUICCases.inst_case_predicate_context /=.
        rewrite - !rename_inst_case_context_wf //.
        { now rewrite -(All2_length X5). }
        eapply forall_P0; tea.
        now eapply on_free_vars_ctx_inst_case_context.
      + cbn.
        rewrite /map_predicate_shift /PCUICCases.inst_case_predicate_context /=.
        rewrite - !rename_inst_case_context_wf //.
        { now rewrite -(All2_length X5). }
        rewrite -heq_pcontext.
        eapply forall_P1; trea.
        × eapply on_contexts_app ⇒ //.
          rewrite {2}heq_pcontext. eapply forall_P0; tea.
          now eapply on_free_vars_ctx_inst_case_context.
        × relativize #|pcontext p0|; [eapply urenaming_context|]; len; trea.
        × rewrite heq_pcontext.
          relativize #|pcontext p1|; [eapply urenaming_context|]; len; trea.
        × relativize #|pcontext p0|. erewrite on_ctx_free_vars_extend, H3. cbn.
          now eapply on_free_vars_ctx_inst_case_context. now len.
      + eapply All2_map.
        eapply forallb_All in p5. eapply All2_All_mix_left in X9; tea.
        eapply (All2_impl X9).
        movex y [] /andP[] onpars onbod [] IHbctx [] [] hbod IHbod eq. unfold on_Trel.
        rewrite /map_predicate_shift /= /inst_case_branch_context /=.
        rewrite - !rename_inst_case_context_wf //.
        { now rewrite -(All2_length X5). }
        split; [|split] ⇒ //.
        × eapply IHbctx; tea.
          now eapply on_free_vars_ctx_inst_case_context.
        × rewrite -eq; eapply IHbod; tea.
          { rewrite {2}eq.
            eapply on_contexts_app ⇒ //.
            eapply IHbctx; tea.
            now eapply on_free_vars_ctx_inst_case_context. }
          { relativize #|bcontext x|; [eapply urenaming_context|]; len; trea. }
          { rewrite eq; relativize #|bcontext y|;[eapply urenaming_context|]; len; trea. }
          { relativize #|bcontext x|. erewrite on_ctx_free_vars_concat, H3.
            rewrite on_free_vars_ctx_on_ctx_free_vars.
            eapply on_free_vars_ctx_inst_case_context; solve_all. now len. }
      
    - rewrite 2!rename_mkApps. simpl. cbn in H0. repeat inv_on_free_vars.
      econstructor; tea.
      3:eapply rename_unfold_cofix; tea.
      all:try rewrite !rename_fix_context.
      + eapply forall_P; tea.
        now eapply on_free_vars_fix_context.
      + eapply All2_All_mix_left in X3; tea.
        eapply All2_map, (All2_impl X3).
        movex y [] /andP[] hty hbody. rewrite /on_Trel.
        move⇒ [] [] Hty IHty [] [] Hbod IHbod /= [=] hna hrarg.
        repeat split; auto. 3:congruence.
        eapply IHty; tea.
        rewrite -(All2_length X3).
        eapply IHbod; tea.
        { eapply on_contexts_app ⇒ //. eapply forall_P; tea.
          now eapply on_free_vars_fix_context. }
        { relativize #|mfix0|; [eapply urenaming_context|]; len; trea. }
        { relativize #|mfix0|; [eapply urenaming_context|]; len; trea.
          now rewrite (All2_length X3). }
        { rewrite -(fix_context_length mfix0). rewrite on_ctx_free_vars_concat H1 /=.
          rewrite on_free_vars_ctx_on_ctx_free_vars. now apply on_free_vars_fix_context. }
      + solve_all.

    - rewrite rename_subst_instance.
      econstructor; tea.
      rewrite rename_closed. 2: assumption.
      eapply (PCUICClosedTyp.declared_constant_closed_body). all: eauto.
    - rewrite rename_mkApps. simpl. cbn in H0; inv_on_free_vars.
      econstructor; tea. 2:erewrite nth_error_map, heq_nth_error; reflexivity.
      solve_all.
    - constructor; eauto.
      eapply forall_P1; tea.
      { constructor; eauto with pcuic. constructor; eauto. }
      { eapply urenaming_vdef; eauto. }
      { eapply urenaming_vdef; eauto. }
      eapply on_ctx_free_vars_snoc_def; eauto.
    - rewrite /map_predicate_shift /=.
      constructor; cbn; eauto.
      all:rewrite /PCUICCases.inst_case_predicate_context /inst_case_branch_context /=.
      all:try rewrite - !rename_inst_case_context_wf //.
      2,4:now rewrite -heq_pcontext - ?(All2_length X1).
      solve_all.
      { eapply forall_P; tea.
        now eapply on_free_vars_ctx_inst_case_context. }
      { relativize #|pcontext p1|. eapply forall_P0; tea.
        + eapply on_contexts_app ⇒ //. eapply forall_P; tea.
          now eapply on_free_vars_ctx_inst_case_context.
        + relativize #|pcontext p0|; [eapply urenaming_context|]; len; trea.
        + relativize #|pcontext p0|; [eapply urenaming_context|]; len; trea.
          now rewrite heq_pcontext.
        + relativize #|pcontext p0|; [erewrite on_ctx_free_vars_concat, H2|]; len; trea.
          relativize #|pcontext p0|; [erewrite on_free_vars_ctx_on_ctx_free_vars|]; len; trea.
          now eapply on_free_vars_ctx_inst_case_context.
        + now rewrite heq_pcontext.
      }
      eapply All2_map; cbn. solve_all.
      all:rewrite - !rename_inst_case_context_wf //.
      1,3:rewrite - ?b -(All2_length X1) //.
      { eapply a0; tea.
        eapply on_free_vars_ctx_inst_case_context; trea. solve_all. }
      { relativize #|bcontext y|; [eapply b0|]; len; trea.
        { eapply on_contexts_app ⇒ //. eapply a0; tea.
          eapply on_free_vars_ctx_inst_case_context; trea. solve_all. }
        { relativize #|bcontext x|; [eapply urenaming_context|]; len; trea. }
        { rewrite /inst_case_branch_context.
          relativize #|bcontext x|; [eapply urenaming_context|]; len; trea.
          now rewrite b. }
        { relativize #|bcontext x|; [erewrite on_ctx_free_vars_concat, H2|]; len; trea.
          rewrite /inst_case_branch_context.
          relativize #|bcontext x|; [erewrite on_free_vars_ctx_on_ctx_free_vars|]; len; trea.
          eapply on_free_vars_ctx_inst_case_context; len; trea.
          solve_all. }
        now rewrite b. }

    - econstructor; tea.
      rewrite !rename_fix_context. eapply forall_P; tea; eauto with fvs.
      rewrite /All2_prop2_eq in X3 ×.
      eapply All2_All_mix_left in X3; tea.
      eapply All2_map, (All2_impl X3).
      movex y [] /andP [] onty onbody. rewrite /on_Trel /=.
      move⇒ [] [] Hty IHty [] [] Hbod IHbod [=] hna hrarg.
      repeat split; try congruence. eauto with fvs.
      rewrite !rename_fix_context.
      relativize #|mfix1|. eapply IHbod; tea.
      { eapply on_contexts_app ⇒ //. eapply forall_P; tea; eauto with fvs. }
      { rewrite -(fix_context_length mfix0). now eapply urenaming_context. }
      { rewrite (All2_length X3) -(fix_context_length mfix1).
        now eapply urenaming_context. }
      { rewrite -(fix_context_length mfix0).
        rewrite on_ctx_free_vars_extend H0 on_free_vars_fix_context //. }
      now rewrite (All2_length X3).
    - econstructor; tea; eauto with fvs.
      eapply forall_P0; tea; eauto with fvs.
      repeat (constructor; eauto).
      1-2:now eapply urenaming_vass.
    - econstructor; tea. solve_all.
    - destruct t ⇒ //; constructor; auto.
  Qed.

  Lemma weakening_pred1 {Σ} {wfΣ : wf Σ} {P Γ Γ' Γ'' Δ Δ' Δ'' M N} :
    pred1 Σ (Γ ,,, Γ') (Δ ,,, Δ') M N
    on_ctx_free_vars (PCUICOnFreeVars.shiftnP #|Γ'| P) (Γ ,,, Γ')
    on_free_vars (PCUICOnFreeVars.shiftnP #|Γ'| P) M
    #|Γ| = #|Δ|
    on_contexts_over (pred1 Σ) Γ Δ Γ'' Δ''
    pred1 Σ (Γ ,,, Γ'' ,,, lift_context #|Γ''| 0 Γ')
          (Δ ,,, Δ'' ,,, lift_context #|Δ''| 0 Δ')
          (lift #|Γ''| #|Γ'| M) (lift #|Δ''| #|Δ'| N).
  Proof.
    intros H onΓ onM hlen predo.
    rewrite !lift_rename.
    pose proof (on_contexts_length predo).
    rewrite -H0.
    pose proof (pred1_pred1_ctx _ H).
    eapply on_contexts_length in X. len in X.
    assert (#|Δ'| = #|Γ'|) by lia. rewrite -H1.
    eapply (fst pred1_rename _ _ _ _ ). tea.
    { pose proof (pred1_pred1_ctx _ H).
      eapply on_contexts_app_inv in X0 as [] ⇒ //.
      eapply on_contexts_app.
      eapply on_contexts_app ⇒ //.
      rewrite - !rename_context_lift_context.
      eapply (snd pred1_rename).
      5:{ eapply on_contexts_app ⇒ //. } exact a.
      2:tea. assumption.
      eapply (weakening_renaming _ Γ []).
      rewrite H0.
      eapply (weakening_renaming _ _ []).
      rewrite on_ctx_free_vars_concat in onΓ.
      move/andP: onΓ⇒ []; eauto.
      rewrite on_ctx_free_vars_concat in onΓ.
      move/andP: onΓ ⇒ [] _.
      now rewrite on_free_vars_ctx_on_ctx_free_vars. }
    rewrite H1. eapply weakening_renaming.
    rewrite H0. apply weakening_renaming.
    2:tea. tea.
  Qed.

  Lemma weakening_pred1_pred1 {Σ} {wfΣ : wf Σ} {P Γ Δ Γ' Δ' M N} :
    pred1_ctx_over Σ Γ Δ Γ' Δ'
    on_ctx_free_vars P Γ
    on_free_vars P M
    pred1 Σ Γ Δ M N
    pred1 Σ (Γ ,,, Γ') (Δ ,,, Δ') (lift0 #|Γ'| M) (lift0 #|Δ'| N).
  Proof.
    intros; eapply (weakening_pred1 (Γ' := []) (Δ' := [])); eauto.
    now rewrite shiftnP0.
    now rewrite shiftnP0.
    pose proof (pred1_pred1_ctx _ X0).
    now rewrite (on_contexts_length X1).
  Qed.

  Lemma weakening_pred1_0 {Σ} {wfΣ : wf Σ} {P Γ Δ Γ' M N} :
    pred1 Σ Γ Δ M N
    on_ctx_free_vars P Γ
    on_free_vars P M
    pred1 Σ (Γ ,,, Γ') (Δ ,,, Γ') (lift0 #|Γ'| M) (lift0 #|Γ'| N).
  Proof.
    intros p onΓ onM.
    eapply weakening_pred1_pred1; tea.
    apply on_contexts_over_refl; pcuic.
  Qed.

  Lemma on_contexts_over_pred1_ctx Σ Γ Γ' Δ Δ' :
    #|Δ| = #|Δ'|
    pred1_ctx Σ (Γ ,,, Δ) (Γ' ,,, Δ')
    All2_fold
      (on_decls (on_decls_over (pred1 Σ) Γ Γ')) Δ Δ'.
  Proof.
    intros. pose proof (on_contexts_length X).
    apply on_contexts_app_inv in X.
    intuition. auto. rewrite !app_context_length in H0. pcuic.
  Qed.
  Hint Resolve on_contexts_over_pred1_ctx : pcuic.

  Lemma nth_error_pred1_ctx_all_defs {P} {Γ Δ} :
    on_contexts P Γ Δ
     i body body', option_map decl_body (nth_error Γ i) = Some (Some body)
              option_map decl_body (nth_error Δ i) = Some (Some body')
              P (skipn (S i) Γ) (skipn (S i) Δ) body body'.
  Proof.
    induction 1; destruct i; simpl; try discriminate; depelim p ⇒ //;
    intros; noconf H; noconf H0; auto.
  Qed.

  Lemma on_contexts_over_firstn_skipn:
     (Σ : global_env) (i : nat) (Δ' R : context),
      pred1_ctx Σ Δ' R
      on_contexts_over (pred1 Σ) (skipn i Δ') (skipn i R) (firstn i Δ') (firstn i R).
  Proof.
    intros Σ i Δ' R redr.
    induction redr in i |- *; simpl.
    × destruct i; constructor; pcuic.
    × destruct i; simpl; constructor; pcuic.
      depelim p; constructor; auto; repeat red; now rewrite /app_context !firstn_skipn.
  Qed.

End ParallelWeakening.

#[global]
Hint Resolve pred1_pred1_ctx : pcuic.

Section ParallelSubstitution.
  Context {cf : checker_flags}.

  Inductive psubst Σ (Γ Γ' : context) : list term list term context context Type :=
  | psubst_empty : psubst Σ Γ Γ' [] [] [] []
  | psubst_vass Δ Δ' s s' na na' t t' T T' :
      psubst Σ Γ Γ' s s' Δ Δ'
      pred1 Σ (Γ ,,, Δ) (Γ' ,,, Δ') T T'
      pred1 Σ Γ Γ' t t'
      psubst Σ Γ Γ' (t :: s) (t' :: s') (Δ ,, vass na T) (Δ' ,, vass na' T')
  | psubst_vdef Δ Δ' s s' na na' t t' T T' :
      psubst Σ Γ Γ' s s' Δ Δ'
      pred1 Σ (Γ ,,, Δ) (Γ' ,,, Δ') T T'
      pred1 Σ Γ Γ' (subst0 s t) (subst0 s' t')
      psubst Σ Γ Γ' (subst0 s t :: s) (subst0 s' t' :: s') (Δ ,, vdef na t T) (Δ' ,, vdef na' t' T').

  Lemma psubst_length {Σ Γ Δ Γ' Δ' s s'} : psubst Σ Γ Δ s s' Γ' Δ'
                                           #|s| = #|Γ'| #|s'| = #|Δ'| #|s| = #|s'|.
  Proof.
    induction 1; simpl; intuition lia.
  Qed.

  Lemma psubst_length' {Σ Γ Δ Γ' Δ' s s'} : psubst Σ Γ Δ s s' Γ' Δ' #|s'| = #|Γ'|.
  Proof.
    induction 1; simpl; lia.
  Qed.

  Lemma psubst_nth_error Σ Γ Δ Γ' Δ' s s' n t :
    psubst Σ Γ Δ s s' Γ' Δ'
    nth_error s n = Some t
     decl decl' t',
      (nth_error Γ' n = Some decl) ×
      (nth_error Δ' n = Some decl') ×
      (nth_error s' n = Some t') ×
    match decl_body decl, decl_body decl' with
    | Some d, Some d'
        let s2 := (skipn (S n) s) in
        let s2' := (skipn (S n) s') in
      let b := subst0 s2 d in
      let b' := subst0 s2' d' in
      psubst Σ Γ Δ s2 s2' (skipn (S n) Γ') (skipn (S n) Δ') ×
      (t = b) × (t' = b') × pred1 Σ Γ Δ t t'
    | None, Nonepred1 Σ Γ Δ t t'
    | _, _False
    end.
  Proof.
    induction 1 in n, t |- *; simpl; auto; destruct n; simpl; try congruence.
    - intros [= <-]. (vass na T), (vass na' T'), t'. intuition auto.
    - intros.
      specialize (IHX _ _ H). intuition eauto.
    - intros [= <-]. (vdef na t0 T), (vdef na' t' T'), (subst0 s' t'). intuition auto.
      simpl. intuition simpl; auto.
    - apply IHX.
  Qed.

  Lemma psubst_nth_error' Σ Γ Δ Γ' Δ' s s' n t :
    psubst Σ Γ Δ s s' Γ' Δ'
    nth_error s n = Some t
     t',
      (nth_error s' n = Some t') ×
      pred1 Σ Γ Δ t t'.
  Proof.
    induction 1 in n, t |- *; simpl; auto; destruct n; simpl; try congruence.
    - intros [= <-]. t'; intuition auto.
    - intros.
      specialize (IHX _ _ H). intuition eauto.
    - intros [= <-]. (subst0 s' t'). intuition auto.
    - apply IHX.
  Qed.

  Lemma psubst_nth_error_None Σ Γ Δ Γ' Δ' s s' n :
    psubst Σ Γ Δ s s' Γ' Δ'
    nth_error s n = None
    (nth_error Γ' n = None) × (nth_error Δ' n = None)* (nth_error s' n = None).
  Proof.
    induction 1 in n |- *; simpl; auto; destruct n; simpl; intros; intuition try congruence.
    - specialize (IHX _ H). intuition congruence.
    - specialize (IHX _ H). intuition congruence.
    - specialize (IHX _ H). intuition congruence.
    - specialize (IHX _ H). intuition congruence.
    - specialize (IHX _ H). intuition congruence.
    - specialize (IHX _ H). intuition congruence.
  Qed.

  Lemma subst_skipn' n s k t : k < n (n - k) #|s|
    lift0 k (subst0 (skipn (n - k) s) t) = subst s k (lift0 n t).
  Proof.
    intros Hk Hn.
    assert (#|firstn (n - k) s| = n - k) by (rewrite firstn_length_le; lia).
    assert (k + (n - k) = n) by lia.
    assert (n - k + k = n) by lia.
    rewrite <- (firstn_skipn (n - k) s) at 2.
    rewrite subst_app_simpl. rewrite H H0.
    rewrite <- (commut_lift_subst_rec t _ n 0 0); try lia.
    generalize (subst0 (skipn (n - k) s) t). intros.
    erewrite <- (simpl_subst_rec _ (firstn (n - k) s) _ k); try lia.
    now rewrite H H1.
  Qed.

  Lemma split_app3 {A} (l l' l'' : list A) (l1 l1' l1'' : list A) :
    #|l| = #|l1| #|l'| = #|l1'|
        l ++ l' ++ l'' = l1 ++ l1' ++ l1''
        l = l1 l' = l1' l'' = l1''.
  Proof.
    intros.
    eapply app_inj_length_l in H1 as [Hl Hr]; auto.
    eapply app_inj_length_l in Hr as [Hl' Hr]; auto.
  Qed.

  Lemma on_contexts_subst_ctx :
     (Σ : global_env) c c0 (Γ0 Δ : context)
    (Γ'0 : list context_decl) (Γ1 Δ1 : context) (Γ'1 : list context_decl) (s s' : list term),
      psubst Σ Γ0 Γ1 s s' Δ Δ1
      #|Γ'0| = #|Γ'1|
      #|Γ0| = #|Γ1|
      on_contexts_over (pred1 Σ) Γ0 Γ1 Δ Δ1
     All2_fold
      (on_decls
       (