Library MetaCoq.PCUIC.PCUICConfluence

From MetaCoq.Template Require Import config utils.
From MetaCoq.PCUIC Require Import PCUICAst PCUICOnOne PCUICAstUtils PCUICTactics PCUICLiftSubst PCUICTyping
     PCUICReduction PCUICEquality PCUICUnivSubstitutionConv
     PCUICSigmaCalculus PCUICContextReduction
     PCUICParallelReduction PCUICParallelReductionConfluence PCUICClosedConv PCUICClosedTyp
     PCUICRedTypeIrrelevance PCUICOnFreeVars PCUICInstDef PCUICInstConv PCUICWeakeningConv PCUICWeakeningTyp.


Require Import ssreflect ssrbool.

From Equations Require Import Equations.
Require Import CRelationClasses CMorphisms.
Require Import Equations.Prop.DepElim.
Require Import Equations.Type.Relation Equations.Type.Relation_Properties.

#[global]
Instance red_Refl Σ Γ : Reflexive (red Σ Γ) := refl_red Σ Γ.

#[global]
Instance red_Trans Σ Γ : Transitive (red Σ Γ) := red_trans Σ Γ.

#[global]
Instance All_decls_refl P :
  Reflexive P
  Reflexive (All_decls P).
Proof. intros hP d; destruct d as [na [b|] ty]; constructor; auto. Qed.

#[global]
Instance All_decls_sym P :
  Symmetric P
  Symmetric (All_decls P).
Proof. intros hP d d' []; constructor; now symmetry. Qed.

#[global]
Instance All_decls_trans P :
  Transitive P
  Transitive (All_decls P).
Proof. intros hP d d' d'' [] h; depelim h; constructor; now etransitivity. Qed.

#[global]
Instance All_decls_equivalence P :
  Equivalence P
  Equivalence (All_decls P).
Proof.
  intros []; split; tc.
Qed.

#[global]
Instance All_decls_preorder P :
  PreOrder P
  PreOrder (All_decls P).
Proof.
  intros []; split; tc.
Qed.

#[global]
Instance All_decls_alpha_refl P :
  Reflexive P
  Reflexive (All_decls_alpha P).
Proof. intros hP d; destruct d as [na [b|] ty]; constructor; auto. Qed.

#[global]
Instance All_decls_alpha_sym P :
  Symmetric P
  Symmetric (All_decls_alpha P).
Proof. intros hP d d' []; constructor; now symmetry. Qed.

#[global]
Instance All_decls_alpha_trans P :
  Transitive P
  Transitive (All_decls_alpha P).
Proof. intros hP d d' d'' [] h; depelim h; constructor; now etransitivity. Qed.

#[global]
Instance All_decls_alpha_equivalence P :
  Equivalence P
  Equivalence (All_decls_alpha P).
Proof.
  intros []; split; tc.
Qed.

Lemma clos_rt_OnOne2_local_env_incl R :
inclusion (OnOne2_local_env (on_one_decl (fun Δclos_refl_trans (R Δ))))
          (clos_refl_trans (OnOne2_local_env (on_one_decl R))).
Proof.
  intros x y H.
  induction H; firstorder; try subst na'.
  - induction b. repeat constructor. pcuicfo.
    constructor 2.
    econstructor 3 with (Γ ,, vass na y); auto.
  - subst.
    induction a0. repeat constructor. pcuicfo.
    constructor 2.
    econstructor 3 with (Γ ,, vdef na b' y); auto.
  - subst t'.
    induction a0. constructor. constructor. red. simpl. pcuicfo.
    constructor 2.
    econstructor 3 with (Γ ,, vdef na y t); auto.
  - clear H. induction IHOnOne2_local_env. constructor. now constructor 3.
    constructor 2.
    eapply transitivity. eauto. auto.
Qed.

Lemma All2_fold_refl {A} {P : list A list A A A Type} :
  ( Γ, Reflexive (P Γ Γ))
  Reflexive (All2_fold P).
Proof.
  intros HR x.
  apply All2_fold_refl; intros. apply HR.
Qed.

Lemma OnOne2_prod {A} (P Q : A A Type) l l' :
  OnOne2 P l l' × OnOne2 Q l l'
  ( x, Q x x)
  OnOne2 (fun x yP x y × Q x y) l l'.
Proof.
  intros [] Hq. induction o. depelim o0. constructor; intuition eauto.
  constructor. split; auto.
  constructor. depelim o0. apply IHo.
  induction tl. depelim o. constructor. auto.
  auto.
Qed.

Lemma OnOne2_prod_assoc {A} (P Q R : A A Type) l l' :
  OnOne2 (fun x y(P x y × Q x y) × R x y) l l'
  OnOne2 P l l' × OnOne2 (fun x yQ x y × R x y) l l'.
Proof.
  induction 1; split; constructor; intuition eauto.
Qed.

Lemma OnOne2_apply {A B} (P : B A A Type) l l' :
  OnOne2 (fun x y a : B, P a x y) l l'
   a : B, OnOne2 (P a) l l'.
Proof.
  induction 1; constructor; auto.
Qed.

Lemma OnOne2_apply_All {A} (Q : A Type) (P : A A Type) l l' :
  OnOne2 (fun x yQ x P x y) l l'
  All Q l
  OnOne2 P l l'.
Proof.
  induction 1; constructor; auto.
  now depelim X. now depelim X0.
Qed.

Lemma OnOne2_sigma {A B} (P : B A A Type) l l' :
  OnOne2 (fun x y a : B, P a x y) l l'
   a : B, OnOne2 (P a) l l'.
Proof.
  induction 1.
  - p.π1. constructor; auto. exact p.π2.
  - IHX.π1. constructor; auto. exact IHX.π2.
Qed.

Lemma OnOne2_local_env_apply {B} {P : B context term term Type} {l l'}
  (f : context term term B) :
  OnOne2_local_env (on_one_decl (fun Γ x y a : B, P a Γ x y)) l l'
  OnOne2_local_env (on_one_decl (fun Γ x yP (f Γ x y) Γ x y)) l l'.
Proof.
  intros; eapply OnOne2_local_env_impl; tea.
  intros Δ x y. eapply on_one_decl_impl; intros Γ ? ?; eauto.
Qed.

Lemma OnOne2_local_env_apply_dep {B : context term term Type}
  {P : context term term Type} {l l'} :
  ( Γ' x y, B Γ' x y)
  OnOne2_local_env (on_one_decl (fun Γ x yB Γ x y P Γ x y)) l l'
  OnOne2_local_env (on_one_decl (fun Γ x yP Γ x y)) l l'.
Proof.
  intros; eapply OnOne2_local_env_impl; tea.
  intros Δ x y. eapply on_one_decl_impl; intros Γ ? ?; eauto.
Qed.

Lemma OnOne2_exist' {A} (P Q R : A A Type) (l l' : list A) :
  OnOne2 P l l'
  ( x y : A, P x y z : A, Q x z × R y z)
   r : list A, OnOne2 Q l r × OnOne2 R l' r.
Proof.
  intros o Hp. induction o.
  - specialize (Hp _ _ p) as [? []].
    eexists; split; constructor; eauto.
  - (hd :: IHo.π1). split; constructor; auto; apply IHo.π2.
Qed.

Lemma OnOne2_local_env_exist' (P Q R : context term term Type) (l l' : context) :
  OnOne2_local_env (on_one_decl P) l l'
  ( Γ x y, P Γ x y z : term, Q Γ x z × R Γ y z)
   r : context, OnOne2_local_env (on_one_decl Q) l r × OnOne2_local_env (on_one_decl R) l' r.
Proof.
  intros o Hp. induction o.
  - destruct p; subst. specialize (Hp _ _ _ p) as [? []].
    eexists; split; constructor; red; cbn; eauto.
  - destruct p; subst.
    destruct s as [[p ->]|[p ->]]; specialize (Hp _ _ _ p) as [? []];
    eexists; split; constructor; red; cbn; eauto.
  - (d :: IHo.π1). split; constructor; auto; apply IHo.π2.
Qed.

Lemma OnOne2_local_env_All2_fold (P : context term term Type)
  (Q : context context context_decl context_decl Type)
  (l l' : context) :
  OnOne2_local_env (on_one_decl P) l l'
  ( Γ x y, on_one_decl P Γ x y Q Γ Γ x y)
  ( Γ Γ' d, OnOne2_local_env (on_one_decl P) Γ Γ' Q Γ Γ' d d)
  ( Γ x, Q Γ Γ x x)
  All2_fold Q l l'.
Proof.
  intros onc HP IHQ HQ. induction onc; simpl; try constructor; eauto.
  now eapply All2_fold_refl.
  now eapply All2_fold_refl.
Qed.

Lemma on_one_decl_compare_decl Σ Re Rle Γ x y :
  RelationClasses.Reflexive Re
  RelationClasses.Reflexive Rle
  on_one_decl
    (fun (_ : context) (y0 v' : term) ⇒ eq_term_upto_univ Σ Re Rle y0 v') Γ x y
  compare_decls (eq_term_upto_univ Σ Re Rle) (eq_term_upto_univ Σ Re Rle) x y.
Proof.
  intros heq hle.
  destruct x as [na [b|] ty], y as [na' [b'|] ty']; cbn; intuition (subst; auto);
  constructor; auto; reflexivity.
Qed.

Lemma OnOne2_disj {A} (P Q : A A Type) (l l' : list A) :
  OnOne2 (fun x yP x y + Q x y)%type l l' <~>
  OnOne2 P l l' + OnOne2 Q l l'.
Proof.
  split.
  - induction 1; [destruct p|destruct IHX]; try solve [(left + right); constructor; auto].
  - intros []; eapply OnOne2_impl; tea; eauto.
Qed.

Notation red1_ctx_rel Σ Δ :=
  (OnOne2_local_env
    (on_one_decl
      (fun (Γ : context) (x0 y0 : term) ⇒ red1 Σ (Δ,,, Γ) x0 y0))).

Notation eq_one_decl Σ Re Rle :=
  (OnOne2_local_env
    (on_one_decl
      (fun _ (x0 y0 : term) ⇒
        eq_term_upto_univ Σ Re Rle x0 y0))).

Lemma red1_eq_context_upto_l {Σ Σ' Rle Re Γ Δ u v} :
  RelationClasses.Reflexive Rle
  SubstUnivPreserving Rle
  RelationClasses.Reflexive Re
  SubstUnivPreserving Re
  RelationClasses.subrelation Re Rle
  red1 Σ Γ u v
  eq_context_upto Σ' Re Rle Γ Δ
   v', red1 Σ Δ u v' ×
        eq_term_upto_univ Σ' Re Re v v'.
Proof.
  intros hle hle' he he' hlee h e.
  induction h in Δ, e |- × using red1_ind_all.
  all: try solve [
    eexists ; split ; [
      solve [ econstructor ; eauto ]
    | eapply eq_term_upto_univ_refl ; eauto
    ]
  ].
  all: try solve [
    destruct (IHh _ e) as [? [? ?]] ;
    eexists ; split ; [
      solve [ econstructor ; eauto ]
    | constructor; eauto ;
      eapply eq_term_upto_univ_refl ; eauto
    ]
  ].
  all: try solve [
    match goal with
    | r : red1 _ (?Γ ,, ?d) _ _ |- _
      assert (e' : eq_context_upto Σ' Re Rle (Γ,, d) (Δ,, d))
      ; [
        constructor ; [ eauto | constructor; eauto ] ;
        eapply eq_term_upto_univ_refl ; eauto
      |
      ]
    end;
    destruct (IHh _ e') as [? [? ?]] ;
    eexists ; split ; [
      solve [ econstructor ; eauto ]
    | constructor ; eauto ;
      eapply eq_term_upto_univ_refl ; eauto
    ]
  ].
  - assert (h : b',
                (option_map decl_body (nth_error Δ i) = Some (Some b')) ×
                eq_term_upto_univ Σ' Re Re body b').
    { induction i in Γ, Δ, H, e |- ×.
      - destruct e.
        + cbn in ×. discriminate.
        + simpl in ×. depelim c; noconf H.
          simpl. eexists; split; eauto.
      - destruct e.
        + cbn in ×. discriminate.
        + simpl in ×. eapply IHi in H ; eauto.
    }
    destruct h as [b' [e1 e2]].
    eexists. split.
    + constructor. eassumption.
    + eapply eq_term_upto_univ_lift ; eauto.
  - eapply OnOne2_prod_inv in X as [_ X].
    eapply OnOne2_apply, OnOne2_apply in X; tea.
    eapply OnOne2_exist' in X as [pars' [parred pareq]]; intros; tea.
    eexists. split. eapply case_red_param; tea.
    econstructor; eauto.
    red. intuition; eauto. reflexivity.
    apply All2_same; intros. intuition eauto; reflexivity.
  - specialize (IHh (Δ ,,, PCUICCases.inst_case_predicate_context p)).
    forward IHh.
    eapply eq_context_upto_cat ⇒ //.
    now apply eq_context_upto_refl.
    destruct IHh as [? [? ?]].
    eexists. split.
    + solve [ econstructor ; eauto ].
    + econstructor; try red; intuition (simpl; eauto); try reflexivity.
      × now eapply All2_same.
      × eapply All2_same. split; reflexivity.
  - specialize (IHh _ e) as [? [? ?]].
    eexists. split.
    + solve [ econstructor ; eauto ].
    + econstructor; try red; intuition (simpl; eauto); try reflexivity.
      × now eapply All2_same.
      × eapply All2_same. split; reflexivity.
  - eapply (OnOne2_impl (Q:=fun x y( v', _) × bcontext x = bcontext y)) in X; tea.
    2:{ intros x y [[red IH] eq]. split; tas.
        specialize (IH (Δ ,,, inst_case_branch_context p x)).
        forward IH by now apply eq_context_upto_cat. exact IH. }
    eapply (OnOne2_exist' _ (fun x yon_Trel_eq (red1 Σ (Δ ,,, inst_case_branch_context p x)) bbody bcontext x y)
      (fun x yon_Trel_eq (eq_term_upto_univ Σ' Re Re) bbody bcontext x y)) in X as [brr [Hred Heq]]; tea.
    2:{ intros x y [[v' [redv' eq]] eqctx].
         {| bcontext := bcontext x; bbody := v' |}.
        intuition auto. }
    eexists; split.
    eapply case_red_brs; tea.
    econstructor; eauto; try reflexivity.
    eapply OnOne2_All2; tea ⇒ /=; intuition eauto; try reflexivity.
    now rewrite b.

  - destruct (IHh _ e) as [x [redl redr]].
     (tApp x M2).
    split. constructor; auto.
    constructor. eapply eq_term_upto_univ_impl. 5:eauto.
    all:auto. 1-3:typeclasses eauto.
    reflexivity.
  - assert (h : ll,
      OnOne2 (red1 Σ Δ) l ll ×
      All2 (eq_term_upto_univ Σ' Re Re) l' ll
    ).
    { induction X.
      - destruct p as [p1 p2].
        eapply p2 in e as hh. destruct hh as [? [? ?]].
        eexists. split.
        + constructor. eassumption.
        + constructor.
          × assumption.
          × eapply All2_same.
            intros.
            eapply eq_term_upto_univ_refl ; eauto.
      - destruct IHX as [ll [? ?]].
        eexists. split.
        + eapply OnOne2_tl. eassumption.
        + constructor ; eauto.
          eapply eq_term_upto_univ_refl ; eauto.
    }
    destruct h as [? [? ?]].
    eexists. split.
    + eapply evar_red. eassumption.
    + constructor. assumption.
  - assert (h : mfix',
      OnOne2 (fun d d'
          red1 Σ Δ d.(dtype) d'.(dtype) ×
          (d.(dname), d.(dbody), d.(rarg)) =
          (d'.(dname), d'.(dbody), d'.(rarg))
        ) mfix0 mfix'
      ×
      All2 (fun x y
        eq_term_upto_univ Σ' Re Re (dtype x) (dtype y) ×
        eq_term_upto_univ Σ' Re Re (dbody x) (dbody y) ×
        (rarg x = rarg y) ×
        (eq_binder_annot (dname x) (dname y)))%type mfix1 mfix').
    { induction X.
      - destruct p as [[p1 p2] p3].
        eapply p2 in e as hh. destruct hh as [? [? ?]].
        eexists. split.
        + constructor.
          instantiate (1 := mkdef _ _ _ _ _).
          split ; eauto.
        + constructor.
          × simpl. repeat split ; eauto.
            eapply eq_term_upto_univ_refl ; eauto.
          × eapply All2_same.
            intros. repeat split ; eauto.
            1-2: eapply eq_term_upto_univ_refl ; eauto.
      - destruct IHX as [? [? ?]].
        eexists. split.
        + eapply OnOne2_tl. eassumption.
        + constructor ; eauto.
          repeat split ; eauto.
          1-2: eapply eq_term_upto_univ_refl ; eauto.
    }
    destruct h as [? [? ?]].
    eexists. split.
    + eapply fix_red_ty. eassumption.
    + constructor. assumption.
  - assert (h : mfix',
      OnOne2 (fun d d'
          red1 Σ (Δ ,,, fix_context mfix0) d.(dbody) d'.(dbody) ×
          (d.(dname), d.(dtype), d.(rarg)) =
          (d'.(dname), d'.(dtype), d'.(rarg))
        ) mfix0 mfix' ×
      All2 (fun x y
        eq_term_upto_univ Σ' Re Re (dtype x) (dtype y) ×
        eq_term_upto_univ Σ' Re Re (dbody x) (dbody y) ×
        (rarg x = rarg y) ×
        eq_binder_annot (dname x) (dname y))%type mfix1 mfix').
    {
      Fail induction X using OnOne2_ind_l.
      change (
        OnOne2
      ((fun L (x y : def term) ⇒
       (red1 Σ (Γ ,,, fix_context L) (dbody x) (dbody y)
        × ( Δ : context,
           eq_context_upto Σ' Re Rle (Γ ,,, fix_context L) Δ
            v' : term,
             red1 Σ Δ (dbody x) v' × eq_term_upto_univ Σ' Re Re (dbody y) v'))
       × (dname x, dtype x, rarg x) = (dname y, dtype y, rarg y)) mfix0) mfix0 mfix1
      ) in X.
      Fail induction X using OnOne2_ind_l.
      revert mfix0 mfix1 X.
      refine (OnOne2_ind_l _ (fun (L : mfixpoint term) (x y : def term) ⇒
    ((red1 Σ (Γ ,,, fix_context L) (dbody x) (dbody y)
     × ( Δ0 : context,
        eq_context_upto Σ' Re Rle (Γ ,,, fix_context L) Δ0
         v' : term,
          red1 Σ Δ0 (dbody x) v' × eq_term_upto_univ Σ' Re Re (dbody y) v'))
    × (dname x, dtype x, rarg x) = (dname y, dtype y, rarg y)))
  (fun L mfix0 mfix1 o mfix' : list (def term),
  OnOne2
      (fun d d' : def term
       red1 Σ (Δ ,,, fix_context L) (dbody d) (dbody d')
       × (dname d, dtype d, rarg d) = (dname d', dtype d', rarg d')) mfix0 mfix'
    × All2
        (fun x y : def term
         ((eq_term_upto_univ Σ' Re Re (dtype x) (dtype y)
          × eq_term_upto_univ Σ' Re Re (dbody x) (dbody y)) ×
         (rarg x = rarg y)) ×
         eq_binder_annot (dname x) (dname y)) mfix1 mfix') _ _).
      - intros L x y l [[p1 p2] p3].
        assert (
           e' : eq_context_upto Σ' Re Rle (Γ ,,, fix_context L) (Δ ,,, fix_context L)
        ).
        { eapply eq_context_upto_cat ; eauto. reflexivity. }
        eapply p2 in e' as hh. destruct hh as [? [? ?]].
        eexists. constructor.
        + constructor.
          instantiate (1 := mkdef _ _ _ _ _).
          split ; eauto.
        + constructor.
          × simpl. repeat split ; eauto.
            eapply eq_term_upto_univ_refl ; eauto.
          × eapply All2_same. intros.
            repeat split ; eauto.
            all: eapply eq_term_upto_univ_refl ; eauto.
      - intros L x l l' h [? [? ?]].
        eexists. constructor.
        + eapply OnOne2_tl. eassumption.
        + constructor ; eauto.
          repeat split ; eauto.
          all: eapply eq_term_upto_univ_refl ; eauto.
    }
    destruct h as [? [? ?]].
    eexists. split.
    + eapply fix_red_body. eassumption.
    + constructor. assumption.
  - assert (h : mfix',
      OnOne2 (fun d d'
          red1 Σ Δ d.(dtype) d'.(dtype) ×
          (d.(dname), d.(dbody), d.(rarg)) =
          (d'.(dname), d'.(dbody), d'.(rarg))
        ) mfix0 mfix' ×
      All2 (fun x y
        eq_term_upto_univ Σ' Re Re (dtype x) (dtype y) ×
        eq_term_upto_univ Σ' Re Re (dbody x) (dbody y) ×
        (rarg x = rarg y) ×
        eq_binder_annot (dname x) (dname y))%type mfix1 mfix'
    ).
    { induction X.
      - destruct p as [[p1 p2] p3].
        eapply p2 in e as hh. destruct hh as [? [? ?]].
        eexists. split.
        + constructor.
          instantiate (1 := mkdef _ _ _ _ _).
          split ; eauto.
        + constructor.
          × simpl. repeat split ; eauto.
            eapply eq_term_upto_univ_refl ; eauto.
          × eapply All2_same.
            intros. repeat split ; eauto.
            all: eapply eq_term_upto_univ_refl ; eauto.
      - destruct IHX as [? [? ?]].
        eexists. split.
        + eapply OnOne2_tl. eassumption.
        + constructor ; eauto.
          repeat split ; eauto.
          all: eapply eq_term_upto_univ_refl ; eauto.
    }
    destruct h as [? [? ?]].
    eexists. split.
    + eapply cofix_red_ty. eassumption.
    + constructor. assumption.
  - assert (h : mfix',
      OnOne2 (fun d d'
          red1 Σ (Δ ,,, fix_context mfix0) d.(dbody) d'.(dbody) ×
          (d.(dname), d.(dtype), d.(rarg)) =
          (d'.(dname), d'.(dtype), d'.(rarg))
        ) mfix0 mfix' ×
      All2 (fun x y
        eq_term_upto_univ Σ' Re Re (dtype x) (dtype y) ×
        eq_term_upto_univ Σ' Re Re (dbody x) (dbody y) ×
        (rarg x = rarg y) ×
        eq_binder_annot (dname x) (dname y))%type mfix1 mfix').
    {
      Fail induction X using OnOne2_ind_l.
      change (
        OnOne2
      ((fun L (x y : def term) ⇒
       (red1 Σ (Γ ,,, fix_context L) (dbody x) (dbody y)
        × ( Δ : context,
           eq_context_upto Σ' Re Rle (Γ ,,, fix_context L) Δ
            v' : term,
             red1 Σ Δ (dbody x) v' × eq_term_upto_univ Σ' Re Re (dbody y) v' ))
       × (dname x, dtype x, rarg x) = (dname y, dtype y, rarg y)) mfix0) mfix0 mfix1
      ) in X.
      Fail induction X using OnOne2_ind_l.
      revert mfix0 mfix1 X.
      refine (OnOne2_ind_l _ (fun (L : mfixpoint term) (x y : def term) ⇒
    (red1 Σ (Γ ,,, fix_context L) (dbody x) (dbody y)
     × ( Δ0 : context,
        eq_context_upto Σ' Re Rle (Γ ,,, fix_context L) Δ0
         v' : term,
           red1 Σ Δ0 (dbody x) v' × eq_term_upto_univ Σ' Re Re (dbody y) v' ))
    × (dname x, dtype x, rarg x) = (dname y, dtype y, rarg y)) (fun L mfix0 mfix1 o mfix' : list (def term),
  (OnOne2
      (fun d d' : def term
       red1 Σ (Δ ,,, fix_context L) (dbody d) (dbody d')
       × (dname d, dtype d, rarg d) = (dname d', dtype d', rarg d')) mfix0 mfix'
    × All2
        (fun x y : def term
         ((eq_term_upto_univ Σ' Re Re (dtype x) (dtype y)
          × eq_term_upto_univ Σ' Re Re (dbody x) (dbody y)) ×
         rarg x = rarg y) ×
         eq_binder_annot (dname x) (dname y)) mfix1 mfix')) _ _).
      - intros L x y l [[p1 p2] p3].
        assert (
           e' : eq_context_upto Σ' Re Rle (Γ ,,, fix_context L) (Δ ,,, fix_context L)
        ).
        { eapply eq_context_upto_cat ; eauto. reflexivity. }
        eapply p2 in e' as hh. destruct hh as [? [? ?]].
        eexists. constructor.
        + constructor.
          instantiate (1 := mkdef _ _ _ _ _).
          split ; eauto.
        + constructor.
          × simpl. repeat split ; eauto.
            eapply eq_term_upto_univ_refl ; eauto.
          × eapply All2_same. intros.
            repeat split ; eauto.
            all: eapply eq_term_upto_univ_refl ; eauto.
      - intros L x l l' h [? [? ?]].
        eexists. constructor.
        + eapply OnOne2_tl. eassumption.
        + constructor ; eauto.
          repeat split ; eauto.
          all: eapply eq_term_upto_univ_refl ; eauto.
    }
    destruct h as [? [? ?]].
    eexists. split.
    + eapply cofix_red_body. eassumption.
    + constructor; assumption.
Qed.

Lemma eq_context_gen_context_assumptions {eq leq Γ Δ} :
  eq_context_gen eq leq Γ Δ
  context_assumptions Γ = context_assumptions Δ.
Proof.
  induction 1; simpl; auto;
  destruct p ⇒ /= //; try lia.
Qed.

Lemma eq_context_extended_subst {Σ Re Rle Γ Δ k} :
  eq_context_gen (eq_term_upto_univ Σ Re Re) (eq_term_upto_univ Σ Re Rle) Γ Δ
  All2 (eq_term_upto_univ Σ Re Re) (extended_subst Γ k) (extended_subst Δ k).
Proof.
  intros Heq.
  induction Heq in k |- *; simpl.
  - constructor; auto.
  - depelim p ⇒ /=.
    × constructor. eauto. constructor; eauto. eauto.
    × constructor.
      + rewrite (eq_context_gen_context_assumptions Heq).
        len. rewrite (All2_fold_length Heq).
        eapply eq_term_upto_univ_substs; eauto. tc.
        eapply eq_term_upto_univ_lift, e0.
      + eapply IHHeq.
Qed.

Lemma eq_context_gen_eq_context_upto Σ Re Rle Γ Γ' :
  RelationClasses.Reflexive Re
  RelationClasses.Reflexive Rle
  eq_context_gen eq eq Γ Γ'
  eq_context_upto Σ Re Rle Γ Γ'.
Proof.
  intros.
  eapply All2_fold_impl; tea.
  cbn; intros ????. move ⇒ []; constructor; subst; auto; reflexivity.
Qed.

Lemma red1_eq_context_upto_univ_l {Σ Σ' Re Rle Γ ctx ctx' ctx''} :
  RelationClasses.Reflexive Re
  RelationClasses.Reflexive Rle
  RelationClasses.Transitive Re
  RelationClasses.Transitive Rle
  SubstUnivPreserving Re
  SubstUnivPreserving Rle
  RelationClasses.subrelation Re Rle
  eq_context_gen (eq_term_upto_univ Σ' Re Re)
   (eq_term_upto_univ Σ' Re Re) ctx ctx'
  OnOne2_local_env (on_one_decl
    (fun (Γ' : context) (u v : term) ⇒
     (Rle : Relation_Definitions.relation Universe.t)
      (napp : nat) (u' : term),
    RelationClasses.Reflexive Re
    RelationClasses.Reflexive Rle
    RelationClasses.Transitive Re
    RelationClasses.Transitive Rle
    SubstUnivPreserving Re
    SubstUnivPreserving Rle
    ( x y : Universe.t, Re x y Rle x y)
    eq_term_upto_univ_napp Σ' Re Rle napp u u'
     v' : term,
      red1 Σ (Γ,,, Γ') u' v'
      × eq_term_upto_univ_napp Σ' Re Rle napp v v')) ctx ctx''
   pctx,
    red1_ctx_rel Σ Γ ctx' pctx ×
    eq_context_gen (eq_term_upto_univ Σ' Re Re) (eq_term_upto_univ Σ' Re Re) ctx'' pctx.
Proof.
  intros.
  rename X into e, X0 into X.
  induction X in e, ctx' |- ×.
  - red in p. simpl in p.
    depelim e. depelim c.
    destruct p as [-> p].
    eapply p in e1 as hh ; eauto.
    destruct hh as [? [? ?]].
    eapply red1_eq_context_upto_l in r; cycle -1.
    { eapply eq_context_upto_cat; tea.
      reflexivity. }
    all:try tc.
    destruct r as [v' [redv' eqv']].
    eexists; split.
    + constructor; tea. red. cbn. split; tea. reflexivity.
    + constructor. all: eauto. constructor; auto.
      now transitivity x.
  - depelim e.
    depelim c.
    destruct p as [-> [[p ->]|[p ->]]].
    { eapply p in e2 as hh ; eauto.
      destruct hh as [? [? ?]].
      eapply red1_eq_context_upto_l in r; cycle -1.
      { eapply eq_context_upto_cat; tea.
        reflexivity. }
      all:try tc.
      destruct r as [v' [redv' eqv']].
      eexists; split.
      + constructor; tea. red. cbn. split; tea. reflexivity.
        left. split; tea. reflexivity.
      + constructor. all: eauto. constructor; auto.
        now transitivity x. }
    { eapply p in e1 as hh ; eauto.
      destruct hh as [? [? ?]].
      eapply red1_eq_context_upto_l in r; cycle -1.
      { eapply eq_context_upto_cat; tea.
        reflexivity. }
      all:try tc.
      destruct r as [v' [redv' eqv']].
      eexists; split.
      + constructor; tea. red. cbn. split; tea. reflexivity.
        right. split; tea. reflexivity.
      + constructor. all: eauto. constructor; auto.
        now transitivity x. }
  - depelim e.
    destruct (IHX _ e) as [? [? ?]].
    eexists. split.
    + now eapply onone2_localenv_cons_tl.
    + constructor. all: eauto.
Qed.


Global Instance eq_context_upto_univ_subst_preserved {cf:checker_flags} Σ
  (Re Rle : ConstraintSet.t Universe.t Universe.t Prop)
  {he: SubstUnivPreserved Re} {hle: SubstUnivPreserved Rle}
  : SubstUnivPreserved (fun φeq_context_upto Σ (Re φ) (Rle φ)).
Proof.
  intros φ φ' u vc Γ Δ eqc.
  eapply All2_fold_map.
  eapply All2_fold_impl; tea.
  cbn; intros.
  destruct X; constructor; cbn; auto; eapply eq_term_upto_univ_subst_preserved; tc; eauto.
Qed.

Lemma eq_context_gen_eq_univ_subst_preserved u Γ Δ :
  eq_context_gen eq eq Γ Δ
  eq_context_gen eq eq (subst_instance u Γ) (subst_instance u Δ).
Proof.
  intros onctx.
  eapply All2_fold_map.
  eapply All2_fold_impl; tea.
  cbn; intros.
  destruct X; constructor; cbn; auto; now subst.
Qed.

Lemma eq_term_upto_univ_subst_instance' {cf:checker_flags} Σ Re Rle :
  RelationClasses.Reflexive Re
  SubstUnivPreserving Re
  RelationClasses.Transitive Re
  RelationClasses.Transitive Rle
  RelationClasses.subrelation Re Rle
  SubstUnivPreserved (fun _Re)
  SubstUnivPreserved (fun _Rle)
   x y napp u1 u2,
    R_universe_instance Re u1 u2
    eq_term_upto_univ_napp Σ Re Rle napp x y
    eq_term_upto_univ_napp Σ Re Rle napp (subst_instance u1 x) (subst_instance u2 y).
Proof.
  intros.
  eapply eq_term_upto_univ_trans with (subst_instance u2 x); tc.
  now eapply eq_term_upto_univ_subst_instance.
  eapply (eq_term_upto_univ_subst_preserved Σ (fun _Re) (fun _Rle) napp ConstraintSet.empty ConstraintSet.empty u2).
  red. destruct check_univs ⇒ //.
  assumption.
Qed.

Lemma eq_context_upto_univ_subst_instance Σ Re Rle :
  RelationClasses.Reflexive Re
  SubstUnivPreserving Re
  RelationClasses.subrelation Re Rle
   x u1 u2,
    R_universe_instance Re u1 u2
    eq_context_upto Σ Re Rle (subst_instance u1 x) (subst_instance u2 x).
Proof.
  intros ref hRe subr t.
  induction t. intros.
  - rewrite /subst_instance /=. constructor.
  - rewrite /subst_instance /=. constructor; auto.
    destruct a as [na [b|] ty]; cbn; constructor; cbn; eauto using eq_term_upto_univ_subst_instance.
    apply eq_term_upto_univ_subst_instance; eauto. tc.
Qed.

Lemma eq_context_upto_univ_subst_instance' Σ Re Rle :
  RelationClasses.Reflexive Re
  RelationClasses.Reflexive Rle
  RelationClasses.Transitive Re
  RelationClasses.Transitive Rle
  SubstUnivPreserving Re
  RelationClasses.subrelation Re Rle
   x y u1 u2,
    R_universe_instance Re u1 u2
    eq_context_gen eq eq x y
    eq_context_upto Σ Re Rle (subst_instance u1 x) (subst_instance u2 y).
Proof.
  intros ref refl' tr trle hRe subr x y u1 u2 ru eqxy.
  eapply All2_fold_trans.
  intros ?????????. eapply compare_decl_trans.
  eapply eq_term_upto_univ_trans; tc.
  eapply eq_term_upto_univ_trans; tc.
  eapply eq_context_gen_eq_context_upto; tea.
  eapply eq_context_gen_eq_univ_subst_preserved; tea.
  eapply eq_context_upto_univ_subst_instance; tc. tea.
Qed.


Lemma red1_eq_term_upto_univ_l {Σ Σ' : global_env} Re Rle napp Γ u v u' :
  RelationClasses.Reflexive Re
  RelationClasses.Reflexive Rle
  RelationClasses.Transitive Re
  RelationClasses.Transitive Rle
  SubstUnivPreserving Re
  SubstUnivPreserving Rle
  RelationClasses.subrelation Re Rle
  eq_term_upto_univ_napp Σ' Re Rle napp u u'
  red1 Σ Γ u v
   v', red1 Σ Γ u' v' ×
         eq_term_upto_univ_napp Σ' Re Rle napp v v'.
Proof.
  intros he he' tRe tRle hle hle' hR e h.
  induction h in napp, u', e, he, he', tRe, tRle, Rle, hle, hle', hR |- × using red1_ind_all.
  all: try solve [
    dependent destruction e ;
    edestruct IHh as [? [? ?]] ; [ .. | eassumption | ] ; eauto ; tc ;
    eexists ; split ; [
      solve [ econstructor ; eauto ]
    | constructor ; eauto
    ]
  ].
  idtac.
  10,15:solve [
    dependent destruction e ;
    edestruct (IHh Rle) as [? [? ?]] ; [ .. | tea | ] ; eauto;
    clear h;
    lazymatch goal with
    | r : red1 _ (?Γ,, vass ?na ?A) ?u ?v,
      e : eq_term_upto_univ_napp _ _ _ _ ?A ?B
      |- _
      let hh := fresh "hh" in
      eapply red1_eq_context_upto_l in r as hh ; revgoals;
      [
        constructor ; [
          eapply (eq_context_upto_refl _ Re Re); eauto
        | constructor; tea
        ]
      | reflexivity
      | assumption
      | assumption
      | assumption
      | assumption
      | destruct hh as [? [? ?]]
]
    end;
    eexists ; split; [ solve [ econstructor ; eauto ]
    | constructor ; eauto ;
      eapply eq_term_upto_univ_trans ; eauto ;
      eapply eq_term_upto_univ_leq ; eauto
    ]
  ].
  - dependent destruction e. dependent destruction e1.
    eexists. split.
    + constructor.
    + eapply eq_term_upto_univ_substs ; eauto.
      eapply leq_term_leq_term_napp; eauto.
  - dependent destruction e.
    eexists. split.
    + constructor.
    + eapply eq_term_upto_univ_substs ; try assumption.
      eapply leq_term_leq_term_napp; eauto.
      auto.
  - dependent destruction e.
    eexists. split.
    + constructor. eassumption.
    + eapply eq_term_upto_univ_refl ; assumption.
  - dependent destruction e.
    apply eq_term_upto_univ_mkApps_l_inv in e0 as [? [? [[h1 h2] h3]]]. subst.
    dependent destruction h1.
    eapply All2_nth_error_Some in a as [t' [hnth [eqctx eqbod]]]; tea.
    have lenctxass := eq_context_gen_context_assumptions eqctx.
    have lenctx := All2_fold_length eqctx.
    eexists. split.
    + constructor; tea.
      epose proof (All2_length h2). congruence.
    + unfold iota_red.
      eapply eq_term_upto_univ_substs ⇒ //.
      { rewrite /expand_lets /expand_lets_k.
        eapply eq_term_upto_univ_substs ⇒ //.
        { simpl. rewrite /inst_case_branch_context !inst_case_context_length.
          rewrite /inst_case_context !context_assumptions_subst_context
            !context_assumptions_subst_instance.
          rewrite lenctxass lenctx.
          eapply eq_term_upto_univ_lift ⇒ //.
          eapply eq_term_upto_univ_leq; tea. lia. }
      eapply eq_context_extended_subst; tea.
      rewrite /inst_case_branch_context.
      eapply eq_context_upto_subst_context; tc.
      eapply eq_context_upto_univ_subst_instance'.
      7,8:tea. all:tc. apply e.
      now eapply All2_rev, e. }
      now eapply All2_rev, All2_skipn.
  - apply eq_term_upto_univ_napp_mkApps_l_inv in e as [? [? [[h1 h2] h3]]]. subst.
    dependent destruction h1.
    unfold unfold_fix in H.
    case_eq (nth_error mfix idx) ;
      try (intros e ; rewrite e in H ; discriminate H).
    intros d e. rewrite e in H. inversion H. subst. clear H.
    eapply All2_nth_error_Some in a as hh ; try eassumption.
    destruct hh as [d' [e' [[[? ?] erarg] eann]]].
    unfold is_constructor in H0.
    case_eq (nth_error args (rarg d)) ;
      try (intros bot ; rewrite bot in H0 ; discriminate H0).
    intros a' ea.
    rewrite ea in H0.
    eapply All2_nth_error_Some in ea as hh ; try eassumption.
    destruct hh as [a'' [ea' ?]].
    eexists. split.
    + eapply red_fix.
      × unfold unfold_fix. rewrite e'; eauto.
      × unfold is_constructor. rewrite <- erarg. rewrite ea'.
        eapply isConstruct_app_eq_term_l ; eassumption.
    + eapply eq_term_upto_univ_napp_mkApps.
      × eapply eq_term_upto_univ_substs ; eauto.
        -- eapply (eq_term_upto_univ_leq _ _ _ 0) ; eauto with arith.
        -- unfold fix_subst.
           apply All2_length in a as el. rewrite <- el.
           generalize #|mfix|. intro n.
           induction n.
           ++ constructor.
           ++ constructor ; eauto.
              constructor. assumption.
      × assumption.
  - dependent destruction e.
    apply eq_term_upto_univ_mkApps_l_inv in e0 as [? [? [[h1 h2] h3]]]. subst.
    dependent destruction h1.
    unfold unfold_cofix in H.
    destruct (nth_error mfix idx) eqn:hnth; noconf H.
    eapply All2_nth_error_Some in a0 as hh ; tea.
    destruct hh as [d' [e' [[[? ?] erarg] eann]]].
    eexists. split.
    + eapply red_cofix_case.
      unfold unfold_cofix. rewrite e'. reflexivity.
    + constructor. all: eauto.
      eapply eq_term_upto_univ_mkApps. all: eauto.
      eapply eq_term_upto_univ_substs ; eauto; try exact _.
      eapply (eq_term_upto_univ_leq _ _ _ 0); auto with arith.
      typeclasses eauto.
      unfold cofix_subst.
      apply All2_length in a0 as el. rewrite <- el.
      generalize #|mfix|. intro n.
      induction n.
      × constructor.
      × constructor ; eauto.
        constructor. assumption.
  - dependent destruction e.
    apply eq_term_upto_univ_mkApps_l_inv in e as [? [? [[h1 h2] h3]]]. subst.
    dependent destruction h1.
    unfold unfold_cofix in H.
    case_eq (nth_error mfix idx) ;
      try (intros e ; rewrite e in H ; discriminate H).
    intros d e. rewrite e in H. inversion H. subst. clear H.
    eapply All2_nth_error_Some in e as hh ; try eassumption.
    destruct hh as [d' [e' [[[? ?] erarg] eann]]].
    eexists. split.
    + eapply red_cofix_proj.
      unfold unfold_cofix. rewrite e'. reflexivity.
    + constructor.
      eapply eq_term_upto_univ_mkApps. all: eauto.
      eapply eq_term_upto_univ_substs ; eauto; try exact _.
      eapply (eq_term_upto_univ_leq _ _ _ 0); auto with arith.
      typeclasses eauto.
      unfold cofix_subst.
      apply All2_length in a as el. rewrite <- el.
      generalize #|mfix|. intro n.
      induction n.
      × constructor.
      × constructor ; eauto.
        constructor. assumption.
  - dependent destruction e.
    eexists. split.
    + econstructor. all: eauto.
    + eapply (eq_term_upto_univ_leq _ _ _ 0); tas. auto. auto with arith.
      now apply eq_term_upto_univ_subst_instance.
  - dependent destruction e.
    apply eq_term_upto_univ_mkApps_l_inv in e as [? [? [[h1 h2] h3]]]. subst.
    dependent destruction h1.
    eapply All2_nth_error_Some in h2 as hh ; try eassumption.
    destruct hh as [arg' [e' ?]].
    eexists. split.
    + constructor. eassumption.
    + eapply eq_term_upto_univ_leq ; eauto.
      eapply eq_term_eq_term_napp; auto. typeclasses eauto.
  - dependent destruction e.
    edestruct IHh as [? [? ?]] ; [ .. | eassumption | ] ; eauto.
    clear h.
    lazymatch goal with
    | r : red1 _ (?Γ,, vdef ?na ?a ?A) ?u ?v,
      e1 : eq_term_upto_univ _ _ _ ?A ?B,
      e2 : eq_term_upto_univ _ _ _ ?a ?b
      |- _
      let hh := fresh "hh" in
      eapply red1_eq_context_upto_l in r as hh ; revgoals ; [
        constructor ; [
          eapply (eq_context_upto_refl _ Re Re) ; eauto
        | econstructor; tea
        ]
      | reflexivity
      | assumption
      | assumption
      | assumption
      | assumption
      | destruct hh as [? [? ?]]
]
     end.
    eexists. split.
    + eapply letin_red_body ; eauto.
    + constructor ; eauto.
      eapply eq_term_upto_univ_trans ; eauto.
      eapply eq_term_upto_univ_leq ; eauto.
  - dependent destruction e.
    destruct e as [? [? [? ?]]].
    eapply OnOne2_prod_inv in X as [_ X].
    assert (h : args,
               OnOne2 (red1 Σ Γ) (pparams p') args ×
               All2 (eq_term_upto_univ Σ' Re Re) params' args
           ).
    { destruct p, p' as []; cbn in ×.
      induction X in a0, pparams, pparams0, X |- ×.
      - depelim a0.
        eapply p in e as hh ; eauto.
        destruct hh as [? [? ?]].
        eexists. split.
        + constructor; tea.
        + constructor. all: eauto.
        + tc.
      - depelim a0.
        destruct (IHX _ a0) as [? [? ?]].
        eexists. split.
        + eapply OnOne2_tl. eassumption.
        + constructor. all: eauto.
    }
    destruct h as [pars0 [? ?]].
    eexists. split.
    + eapply case_red_param. eassumption.
    + constructor. all: eauto.
      red; intuition eauto.
  - depelim e.
    destruct e as [? [? [? ?]]].
    eapply IHh in e ⇒ //.
    destruct e as [v' [red eq]].
    eapply red1_eq_context_upto_l in red.
    7:{ eapply eq_context_upto_cat.
        2:{ instantiate (1:=PCUICCases.inst_case_predicate_context p').
            rewrite /inst_case_predicate_context /inst_case_context.
            eapply eq_context_upto_subst_context; tc.
            eapply eq_context_upto_univ_subst_instance'.
            7,8:tea. all:tc.
            now eapply All2_rev. }
        eapply eq_context_upto_refl; tc. }
    all:tc.
    destruct red as [ret' [redret eqret]].
    eexists; split.
    + eapply case_red_return; tea.
    + econstructor; eauto.
      red; simpl; intuition eauto.
      now transitivity v'.

  - depelim e.
    eapply OnOne2_prod_assoc in X as [_ X].
    assert (h : brs0,
          OnOne2 (fun br br'
            on_Trel_eq (red1 Σ (Γ ,,, inst_case_branch_context p' br)) bbody bcontext br br') brs' brs0 ×
          All2 (fun x y
            eq_context_gen eq eq (bcontext x) (bcontext y) ×
            (eq_term_upto_univ Σ' Re Re (bbody x) (bbody y))
            )%type brs'0 brs0
        ).
      { induction X in a, brs' |- ×.
        - destruct p0 as [p2 p3].
          dependent destruction a. destruct p0 as [h1 h2].
          eapply p2 in h2 as hh ; eauto.
          destruct hh as [? [? ?]].
          eapply (red1_eq_context_upto_l (Re:=Re) (Rle:=Rle) (Δ := Γ ,,, inst_case_branch_context p' y)) in r; cycle -1.
          { eapply eq_context_upto_cat; tea. reflexivity.
            rewrite /inst_case_branch_context /inst_case_context.
            eapply eq_context_upto_subst_context; tc.
            eapply eq_context_upto_univ_subst_instance'. 7,8:tea. all:tc.
            apply e. apply All2_rev, e. }
          all:tc.
          destruct r as [v' [redv' eqv']].
          eexists. split.
          + constructor.
            instantiate (1 := {| bcontext := bcontext y; bbody := v' |}). cbn. split ; eauto.
          + constructor. all: eauto.
            split ; eauto. cbn. transitivity (bcontext hd) ; eauto.
            now rewrite p3. simpl. now transitivity x.
        - dependent destruction a.
          destruct (IHX _ a) as [? [? ?]].
          eexists. split.
          + eapply OnOne2_tl. eassumption.
          + constructor. all: eauto.
      }
      destruct h as [brs0 [? ?]].
      eexists. split.
      × eapply case_red_brs; tea.
      × constructor. all: eauto.

  - dependent destruction e.
    assert (h : args,
               OnOne2 (red1 Σ Γ) args' args ×
               All2 (eq_term_upto_univ Σ' Re Re) l' args
           ).
    { induction X in a, args' |- ×.
      - destruct p as [p1 p2].
        dependent destruction a.
        eapply p2 in e as hh ; eauto.
        destruct hh as [? [? ?]].
        eexists. split.
        + constructor. eassumption.
        + constructor. all: eauto.
        + tc.
      - dependent destruction a.
        destruct (IHX _ a) as [? [? ?]].
        eexists. split.
        + eapply OnOne2_tl. eassumption.
        + constructor. all: eauto.
    }
    destruct h as [? [? ?]].
    eexists. split.
    + eapply evar_red. eassumption.
    + constructor. all: eauto.
  - dependent destruction e.
    assert (h : mfix,
               OnOne2 (fun d0 d1
                   red1 Σ Γ d0.(dtype) d1.(dtype) ×
                   (d0.(dname), d0.(dbody), d0.(rarg)) =
                   (d1.(dname), d1.(dbody), d1.(rarg))
                 ) mfix' mfix ×
               All2 (fun x y
                 eq_term_upto_univ Σ' Re Re x.(dtype) y.(dtype) ×
                 eq_term_upto_univ Σ' Re Re x.(dbody) y.(dbody) ×
                 (x.(rarg) = y.(rarg)) ×
                 eq_binder_annot (dname x) (dname y))%type mfix1 mfix
           ).
    { induction X in a, mfix' |- ×.
      - destruct p as [[p1 p2] p3].
        dependent destruction a.
        destruct p as [[[h1 h2] h3] h4].
        eapply p2 in h1 as hh ; eauto.
        destruct hh as [? [? ?]].
        eexists. split.
        + constructor.
          instantiate (1 := mkdef _ _ _ _ _).
          simpl. eauto.
        + constructor. all: eauto.
          simpl. inversion p3.
          repeat split ; eauto.
        + tc.
      - dependent destruction a. destruct p as [[[h1 h2] h3] h4].
        destruct (IHX _ a) as [? [? ?]].
        eexists. split.
        + eapply OnOne2_tl. eassumption.
        + constructor. all: eauto.
    }
    destruct h as [? [? ?]].
    eexists. split.
    + eapply fix_red_ty. eassumption.
    + constructor. all: eauto.
  - dependent destruction e.
    assert (h : mfix,
               OnOne2 (fun x y
                   red1 Σ (Γ ,,, fix_context mfix0) x.(dbody) y.(dbody) ×
                   (dname x, dtype x, rarg x) = (dname y, dtype y, rarg y)
                 ) mfix' mfix ×
               All2 (fun x y
                 eq_term_upto_univ Σ' Re Re x.(dtype) y.(dtype) ×
                 eq_term_upto_univ Σ' Re Re x.(dbody) y.(dbody) ×
                 (x.(rarg) = y.(rarg)) ×
                 eq_binder_annot (dname x) (dname y)) mfix1 mfix
           ).
    { revert mfix' a.
      refine (OnOne2_ind_l _ (fun L x y(red1 Σ (Γ ,,, fix_context L) (dbody x) (dbody y)
        × ( Rle napp (u' : term),
           RelationClasses.Reflexive Re
           RelationClasses.Reflexive Rle
           RelationClasses.Transitive Re
           RelationClasses.Transitive Rle
           SubstUnivPreserving Re
           SubstUnivPreserving Rle
           ( u u'0 : Universe.t, Re u u'0 Rle u u'0)
           eq_term_upto_univ_napp Σ' Re Rle napp (dbody x) u'
            v' : term,
             red1 Σ (Γ ,,, fix_context L) u' v'
                  × eq_term_upto_univ_napp Σ' Re Rle napp (dbody y) v' ))
       × (dname x, dtype x, rarg x) = (dname y, dtype y, rarg y)) (fun L mfix0 mfix1 o mfix', All2
      (fun x y : def term
       ((eq_term_upto_univ Σ' Re Re (dtype x) (dtype y)
        × eq_term_upto_univ Σ' Re Re (dbody x) (dbody y)) ×
       rarg x = rarg y) × eq_binder_annot (dname x) (dname y)) mfix0 mfix' mfix : list (def term),
  ( OnOne2
      (fun x y : def term
       red1 Σ (Γ ,,, fix_context L) (dbody x) (dbody y)
       × (dname x, dtype x, rarg x) = (dname y, dtype y, rarg y)) mfix' mfix ) ×
  ( All2
      (fun x y : def term
       ((eq_term_upto_univ Σ' Re Re (dtype x) (dtype y)
        × eq_term_upto_univ Σ' Re Re (dbody x) (dbody y)) ×
       (rarg x = rarg y)) × eq_binder_annot (dname x) (dname y)) mfix1 mfix )) _ _ _ _ X).
      - clear X. intros L x y l [[p1 p2] p3] mfix' h.
        dependent destruction h. destruct p as [[[h1 h2] h3] h4].
        eapply p2 in h2 as hh ; eauto.
        destruct hh as [? [? ?]].
        eexists. split.
        + constructor. constructor.
          instantiate (1 := mkdef _ _ _ _ _).
          simpl. eauto. reflexivity.
        + constructor. constructor; simpl. all: eauto.
          inversion p3.
          simpl. repeat split ; eauto. destruct y0. simpl in ×.
          congruence.
      - clear X. intros L x l l' h ih mfix' ha.
        dependent destruction ha. destruct p as [[h1 h2] h3].
        destruct (ih _ ha) as [? [? ?]].
        eexists. split.
        + eapply OnOne2_tl. eauto.
        + constructor. constructor. all: eauto.
    }
    destruct h as [mfix [? ?]].
    assert (h : mfix,
      OnOne2 (fun x y
                  red1 Σ (Γ ,,, fix_context mfix') x.(dbody) y.(dbody) ×
                  (dname x, dtype x, rarg x) = (dname y, dtype y, rarg y)
               ) mfix' mfix ×
        All2 (fun x y
                eq_term_upto_univ Σ' Re Re x.(dtype) y.(dtype) ×
                eq_term_upto_univ Σ' Re Re x.(dbody) y.(dbody) ×
                (x.(rarg) = y.(rarg)) ×
                eq_binder_annot (dname x) (dname y)
             ) mfix1 mfix %type
    ).
    { clear X.
      assert (hc : eq_context_upto Σ'
                     Re Rle
                     (Γ ,,, fix_context mfix0)
                     (Γ ,,, fix_context mfix')
             ).
      { eapply eq_context_upto_cat.
        - eapply eq_context_upto_refl; assumption.
        - clear -he hle tRe tRle hR a. induction a.
          + constructor.
          + destruct r as [[[? ?] ?] ?].
            eapply All2_eq_context_upto.
            eapply All2_rev.
            eapply All2_mapi.
            constructor.
            × intros i. split; [split|]; cbn.
              -- assumption.
              -- cbn. constructor.
              -- cbn. eapply eq_term_upto_univ_lift.
                 eapply eq_term_upto_univ_impl; eauto.
                 all:typeclasses eauto.
            × eapply All2_impl ; eauto.
              intros ? ? [[[? ?] ?] ?] i. split; [split|].
              -- assumption.
              -- cbn. constructor.
              -- cbn. eapply eq_term_upto_univ_lift.
                 eapply eq_term_upto_univ_impl; eauto.
                 typeclasses eauto.
      }
      clear a.
      eapply OnOne2_impl_exist_and_All ; try eassumption.
      clear o a0.
      intros x x' y [r e] [[[? ?] ?] ?].
      inversion e. clear e.
      eapply red1_eq_context_upto_l in r as [? [? ?]].
      7: eassumption. all: tea.
      eexists. constructor.
      instantiate (1 := mkdef _ _ _ _ _). simpl.
      intuition eauto.
      intuition eauto.
      - rewrite H1. eauto.
      - eapply eq_term_upto_univ_trans; tea.
      - etransitivity ; eauto.
      - now simpl.
    }
    destruct h as [? [? ?]].
    eexists. split.
    + eapply fix_red_body. eassumption.
    + constructor. all: eauto.
  - dependent destruction e.
    assert (h : mfix,
               OnOne2 (fun d0 d1
                   red1 Σ Γ d0.(dtype) d1.(dtype) ×
                   (d0.(dname), d0.(dbody), d0.(rarg)) =
                   (d1.(dname), d1.(dbody), d1.(rarg))
                 ) mfix' mfix ×
               All2 (fun x y
                 eq_term_upto_univ Σ' Re Re x.(dtype) y.(dtype) ×
                 eq_term_upto_univ Σ' Re Re x.(dbody) y.(dbody) ×
                 (x.(rarg) = y.(rarg)) ×
                 eq_binder_annot (dname x) (dname y))%type mfix1 mfix
           ).
    { induction X in a, mfix' |- ×.
      - destruct p as [[p1 p2] p3].
        dependent destruction a.
        destruct p as [[[h1 h2] h3] h4].
        eapply p2 in h1 as hh ; eauto.
        destruct hh as [? [? ?]].
        eexists. split.
        + constructor.
          instantiate (1 := mkdef _ _ _ _ _).
          simpl. eauto.
        + constructor. all: eauto.
          simpl. inversion p3.
          repeat split ; eauto.
        + tc.
      - dependent destruction a. destruct p as [[h1 h2] h3].
        destruct (IHX _ a) as [? [? ?]].
        eexists. split.
        + eapply OnOne2_tl. eassumption.
        + constructor. all: eauto.
    }
    destruct h as [? [? ?]].
    eexists. split.
    + eapply cofix_red_ty. eassumption.
    + constructor. all: eauto.
  - dependent destruction e.
    assert (h : mfix,
               OnOne2 (fun x y
                   red1 Σ (Γ ,,, fix_context mfix0) x.(dbody) y.(dbody) ×
                   (dname x, dtype x, rarg x) = (dname y, dtype y, rarg y)
                 ) mfix' mfix ×
               All2 (fun x y
                 eq_term_upto_univ Σ' Re Re x.(dtype) y.(dtype) ×
                 eq_term_upto_univ Σ' Re Re x.(dbody) y.(dbody) ×
                 (x.(rarg) = y.(rarg)) ×
                 eq_binder_annot (dname x) (dname y)
               ) mfix1 mfix
           ).
    { revert mfix' a.
      refine (OnOne2_ind_l _ (fun L x y(red1 Σ (Γ ,,, fix_context L) (dbody x) (dbody y)
        × ( Rle napp (u' : term),
            RelationClasses.Reflexive Re
            RelationClasses.Reflexive Rle
            RelationClasses.Transitive Re
            RelationClasses.Transitive Rle
            SubstUnivPreserving Re
            SubstUnivPreserving Rle
           ( u u'0 : Universe.t, Re u u'0 Rle u u'0)
           eq_term_upto_univ_napp Σ' Re Rle napp (dbody x) u'
            v' : term,
             red1 Σ (Γ ,,, fix_context L) u' v'
               × eq_term_upto_univ_napp Σ' Re Rle napp (dbody y) v'))
       × (dname x, dtype x, rarg x) = (dname y, dtype y, rarg y)) (fun L mfix0 mfix1 o mfix', All2
      (fun x y : def term
       ((eq_term_upto_univ Σ' Re Re (dtype x) (dtype y)
        × eq_term_upto_univ Σ' Re Re (dbody x) (dbody y)) ×
       rarg x = rarg y) × eq_binder_annot (dname x) (dname y)) mfix0 mfix' mfix : list (def term),
  ( OnOne2
      (fun x y : def term
       red1 Σ (Γ ,,, fix_context L) (dbody x) (dbody y)
       × (dname x, dtype x, rarg x) = (dname y, dtype y, rarg y)) mfix' mfix ) ×
  ( All2
      (fun x y : def term
       ((eq_term_upto_univ Σ' Re Re (dtype x) (dtype y)
        × eq_term_upto_univ Σ' Re Re (dbody x) (dbody y)) ×
       rarg x = rarg y) × eq_binder_annot (dname x) (dname y)) mfix1 mfix )) _ _ _ _ X).
      - clear X. intros L x y l [[p1 p2] p3] mfix' h.
        dependent destruction h. destruct p as [[[h1 h2] h3] h4].
        eapply p2 in h2 as hh ; eauto.
        destruct hh as [? [? ?]].
        noconf p3. hnf in H. noconf H.
        eexists. split; simpl.
        + constructor.
          instantiate (1 := mkdef _ _ _ _ _).
          simpl. eauto.
        + constructor. all: eauto.
          simpl. repeat split ; eauto; congruence.
      - clear X. intros L x l l' h ih mfix' ha.
        dependent destruction ha. destruct p as [[h1 h2] h3].
        destruct (ih _ ha) as [? [? ?]].
        eexists. split.
        + eapply OnOne2_tl. eauto.
        + constructor. all: eauto.
    }
    destruct h as [mfix [? ?]].
    assert (h : mfix,
      OnOne2 (fun x y
                  red1 Σ (Γ ,,, fix_context mfix') x.(dbody) y.(dbody) ×
                  (dname x, dtype x, rarg x) = (dname y, dtype y, rarg y)
               ) mfix' mfix ×
        All2 (fun x y
                eq_term_upto_univ Σ' Re Re x.(dtype) y.(dtype) ×
                eq_term_upto_univ Σ' Re Re x.(dbody) y.(dbody) ×
                (x.(rarg) = y.(rarg)) ×
                eq_binder_annot (dname x) (dname y)
             ) mfix1 mfix
    ).
    { clear X.
      assert (hc : eq_context_upto Σ'
                     Re Rle
                     (Γ ,,, fix_context mfix0)
                     (Γ ,,, fix_context mfix')
             ).
      { eapply eq_context_upto_cat.
        - eapply eq_context_upto_refl; assumption.
        - clear -he he' hle hle' hR a. induction a.
          + constructor.
          + destruct r as [[[? ?] ?] ?].
            eapply All2_eq_context_upto.
            eapply All2_rev.
            eapply All2_mapi.
            constructor.
            × intros i. split; [split|].
              -- assumption.
              -- cbn. constructor.
              -- cbn. eapply eq_term_upto_univ_lift.
                 eapply eq_term_upto_univ_impl; eauto.
                 all:typeclasses eauto.
            × eapply All2_impl ; eauto.
              intros ? ? [[[? ?] ?] ?] i. split; [split|].
              -- assumption.
              -- cbn. constructor.
              -- cbn. eapply eq_term_upto_univ_lift.
                 eapply eq_term_upto_univ_impl; eauto.
                 all:typeclasses eauto.
      }
      clear a.
      eapply OnOne2_impl_exist_and_All ; try eassumption.
      clear o a0.
      intros x x' y [r e] [[? ?] ?].
      inversion e. clear e.
      eapply red1_eq_context_upto_l in r as [? [? ?]].
      7: eassumption. all: tea.
      eexists.
      instantiate (1 := mkdef _ _ _ _ _). simpl.
      intuition eauto.
      - rewrite H1. eauto.
      - eapply eq_term_upto_univ_trans ; tea.
      - etransitivity ; eauto.
      - congruence.
    }
    destruct h as [? [? ?]].
    eexists. split.
    + eapply cofix_red_body. eassumption.
    + constructor. all: eauto.
Qed.

Lemma Forall2_flip {A} (R : A A Prop) (x y : list A) :
  Forall2 (flip R) y x Forall2 R x y.
Proof.
  induction 1; constructor; auto.
Qed.

Lemma R_universe_instance_flip R u u' :
  R_universe_instance (flip R) u' u
  R_universe_instance R u u'.
Proof.
  unfold R_universe_instance.
  apply Forall2_flip.
Qed.

Lemma eq_context_upto_flip {Σ Re Rle Γ Δ}
  `{!RelationClasses.Reflexive Re}
  `{!RelationClasses.Symmetric Re}
  `{!RelationClasses.Transitive Re}
  `{!RelationClasses.Reflexive Rle}
  `{!RelationClasses.Transitive Rle}
  `{!RelationClasses.subrelation Re Rle} :
  eq_context_upto Σ Re Rle Γ Δ
  eq_context_upto Σ Re (flip Rle) Δ Γ.
Proof.
  induction 1; constructor; auto; depelim p; constructor; auto.
  - now symmetry.
  - now eapply eq_term_upto_univ_napp_flip; try typeclasses eauto.
  - now symmetry.
  - now eapply eq_term_upto_univ_napp_flip; try typeclasses eauto.
  - now eapply eq_term_upto_univ_napp_flip; try typeclasses eauto.
Qed.

Lemma red1_eq_context_upto_r {Σ Σ' Re Rle Γ Δ u v} :
  RelationClasses.Equivalence Re
  RelationClasses.PreOrder Rle
  SubstUnivPreserving Re
  SubstUnivPreserving Rle
  RelationClasses.subrelation Re Rle
  red1 Σ Γ u v
  eq_context_upto Σ' Re Rle Δ Γ
   v', red1 Σ Δ u v' ×
        eq_term_upto_univ Σ' Re Re v' v.
Proof.
  intros.
  destruct (@red1_eq_context_upto_l Σ Σ' (flip Rle) Re Γ Δ u v); auto; try typeclasses eauto.
  - intros x; red; reflexivity.
  - intros s u1 u2 Ru. red. apply R_universe_instance_flip in Ru. now apply H2.
  - intros x y rxy; red. now symmetry in rxy.
  - now apply eq_context_upto_flip.
  - x. intuition auto.
    now eapply eq_term_upto_univ_sym.
Qed.

Lemma red1_eq_term_upto_univ_r {Σ Σ' Re Rle napp Γ u v u'} :
  RelationClasses.Reflexive Re
  RelationClasses.Reflexive Rle
  RelationClasses.Symmetric Re
  RelationClasses.Transitive Re
  RelationClasses.Transitive Rle
  SubstUnivPreserving Re
  SubstUnivPreserving Rle
  RelationClasses.subrelation Re Rle
  eq_term_upto_univ_napp Σ' Re Rle napp u' u
  red1 Σ Γ u v
   v', red1 Σ Γ u' v' ×
        eq_term_upto_univ_napp Σ' Re Rle napp v' v.
Proof.
  intros he he' hse hte htle sre srle hR h uv.
  destruct (@red1_eq_term_upto_univ_l Σ Σ' Re (flip Rle) napp Γ u v u'); auto.
  - now eapply flip_Transitive.
  - red. intros s u1 u2 ru.
    apply R_universe_instance_flip in ru.
    now apply srle.
  - intros x y X. symmetry in X. apply hR in X. apply X.
  - eapply eq_term_upto_univ_napp_flip; eauto.
  - x. intuition auto.
    eapply (@eq_term_upto_univ_napp_flip Σ' Re (flip Rle) Rle); eauto.
    + now eapply flip_Transitive.
    + unfold flip. intros ? ? H. symmetry in H. eauto.
Qed.

Section RedEq.
  Context (Σ : global_env_ext).
  Context {Re Rle : Universe.t Universe.t Prop}
          {refl : RelationClasses.Reflexive Re}
          {refl': RelationClasses.Reflexive Rle}
          {pres : SubstUnivPreserving Re}
          {pres' : SubstUnivPreserving Rle}
          {sym : RelationClasses.Symmetric Re}
          {trre : RelationClasses.Transitive Re}
          {trle : RelationClasses.Transitive Rle}.
  Context (inclre : RelationClasses.subrelation Re Rle).

  Lemma red_eq_term_upto_univ_r {Γ T V U} :
    eq_term_upto_univ Σ Re Rle T U red Σ Γ U V
     T', red Σ Γ T T' × eq_term_upto_univ Σ Re Rle T' V.
  Proof using inclre pres pres' refl refl' sym trle trre.
    intros eq r.
    induction r in T, eq |- ×.
    - eapply red1_eq_term_upto_univ_r in eq as [v' [r' eq']]; eauto.
    - T; split; eauto.
    - case: (IHr1 _ eq) ⇒ T' [r' eq'].
      case: (IHr2 _ eq') ⇒ T'' [r'' eq''].
       T''. split=>//.
      now transitivity T'.
  Qed.

  Lemma red_eq_term_upto_univ_l {Γ u v u'} :
    eq_term_upto_univ Σ Re Rle u u'
    red Σ Γ u v
     v',
    red Σ Γ u' v' ×
    eq_term_upto_univ Σ Re Rle v v'.
  Proof using inclre pres pres' refl refl' trle trre.
    intros eq r.
    induction r in u', eq |- ×.
    - eapply red1_eq_term_upto_univ_l in eq as [v' [r' eq']]; eauto.
    - u'. split; auto.
    - case: (IHr1 _ eq) ⇒ T' [r' eq'].
      case: (IHr2 _ eq') ⇒ T'' [r'' eq''].
       T''. split=>//.
      now transitivity T'.
  Qed.
End RedEq.

Polymorphic Derive Signature for Relation.clos_refl_trans.

Derive Signature for red1.

Lemma local_env_telescope P Γ Γ' Δ Δ' :
  All2_telescope (on_decls P) Γ Γ' Δ Δ'
  on_contexts_over P Γ Γ' (List.rev Δ) (List.rev Δ').
Proof.
  induction 1. simpl. constructor.
  - depelim p. simpl. eapply on_contexts_over_app. repeat constructor ⇒ //.
    simpl.
    revert IHX.
    generalize (List.rev Δ) (List.rev Δ'). induction 1. constructor.
    constructor; auto. depelim p0; constructor; auto;
    now rewrite !app_context_assoc.
  - simpl. eapply on_contexts_over_app. constructor. 2:auto. constructor.
    simpl. depelim p.
    revert IHX.
    generalize (List.rev Δ) (List.rev Δ'). induction 1. constructor.
    constructor; auto. depelim p1; constructor; auto;
    now rewrite !app_context_assoc.
Qed.

Lemma All_All2_telescopei_gen P (Γ Γ' Δ Δ' : context) (m m' : mfixpoint term) :
  ( Δ Δ' x y,
    on_contexts_over P Γ Γ' Δ Δ'
    P Γ Γ' x y
    P (Γ ,,, Δ) (Γ' ,,, Δ') (lift0 #|Δ| x) (lift0 #|Δ'| y))
  All2 (on_Trel_eq (P Γ Γ') dtype dname) m m'
  on_contexts_over P Γ Γ' Δ Δ'
  All2_telescope_n (on_decls P) (fun n : natlift0 n)
                   (Γ ,,, Δ) (Γ' ,,, Δ') #|Δ|
    (map (fun def : def termvass (dname def) (dtype def)) m)
    (map (fun def : def termvass (dname def) (dtype def)) m').
Proof.
  intros weakP.
  induction 1 in Δ, Δ' |- *; cbn. constructor.
  intros. destruct r. rewrite e. constructor.
  constructor.
  rewrite {2}(All2_fold_length X0).
  now eapply weakP.
  specialize (IHX (vass (dname y) (lift0 #|Δ| (dtype x)) :: Δ)
                  (vass (dname y) (lift0 #|Δ'| (dtype y)) :: Δ')).
  forward IHX.
  constructor; auto. constructor. now eapply weakP. simpl in IHX.
  rewrite {2}(All2_fold_length X0).
  apply IHX.
Qed.

Lemma All_All2_telescopei P (Γ Γ' : context) (m m' : mfixpoint term) :
  ( Δ Δ' x y,
    on_contexts_over P Γ Γ' Δ Δ'
    P Γ Γ' x y
    P (Γ ,,, Δ) (Γ' ,,, Δ') (lift0 #|Δ| x) (lift0 #|Δ'| y))
  All2 (on_Trel_eq (P Γ Γ') dtype dname) m m'
  All2_telescope_n (on_decls P) (fun nlift0 n)
                   Γ Γ' 0
                   (map (fun defvass (dname def) (dtype def)) m)
                   (map (fun defvass (dname def) (dtype def)) m').
Proof.
  specialize (All_All2_telescopei_gen P Γ Γ' [] [] m m'). simpl.
  intros. specialize (X X0 X1). apply X; constructor.
Qed.

Lemma All2_All2_fold_fix_context P (Γ Γ' : context) (m m' : mfixpoint term) :
  ( Δ Δ' x y,
    on_contexts_over P Γ Γ' Δ Δ'
    P Γ Γ' x y
    P (Γ ,,, Δ) (Γ' ,,, Δ') (lift0 #|Δ| x) (lift0 #|Δ'| y))
  All2 (on_Trel_eq (P Γ Γ') dtype dname) m m'
  All2_fold (on_decls (on_decls_over P Γ Γ')) (fix_context m) (fix_context m').
Proof.
  intros Hweak a. unfold fix_context.
  eapply local_env_telescope.
  cbn.
  rewrite - !(mapi_mapi
                (fun n defvass (dname def) (dtype def))
                (fun n decllift_decl n 0 decl)).
  eapply All2_telescope_mapi.
  rewrite !mapi_cst_map.
  eapply All_All2_telescopei; eauto.
Qed.

Lemma OnOne2_pars_pred1_ctx_over {cf : checker_flags} {Σ} {wfΣ : wf Σ} Γ params params' puinst pctx :
  on_ctx_free_vars xpredT Γ
  forallb (on_free_vars xpredT) params
  on_free_vars_ctx (shiftnP #|params| xpredT) pctx
  OnOne2 (pred1 Σ Γ Γ) params params'
  pred1_ctx_over Σ Γ Γ (inst_case_context params puinst pctx) (inst_case_context params' puinst pctx).
Proof.
  intros onΓ onpars onpctx redp.
  eapply OnOne2_All2 in redp.
  eapply pred1_ctx_over_inst_case_context; tea.
  all:pcuic.
Qed.

Lemma on_free_vars_ctx_closed_xpredT n ctx :
  on_free_vars_ctx (closedP n xpredT) ctx
  on_free_vars_ctx xpredT ctx.
Proof.
  eapply on_free_vars_ctx_impl ⇒ //.
Qed.

Lemma on_ctx_free_vars_inst_case_context_xpredT (Γ : list context_decl) (pars : list term)
  (puinst : Instance.t) (pctx : list context_decl) :
  forallb (on_free_vars xpredT) pars
  on_free_vars_ctx (closedP #|pars| xpredT) pctx
  on_ctx_free_vars xpredT Γ
  on_ctx_free_vars xpredT
    (Γ,,, inst_case_context pars puinst pctx).
Proof.
  intros.
  rewrite -(shiftnP_xpredT #|pctx|).
  apply on_ctx_free_vars_inst_case_context ⇒ //.
  rewrite test_context_k_closed_on_free_vars_ctx //.
Qed.

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

Lemma on_ctx_free_vars_fix_context_xpredT (Γ : list context_decl) mfix :
  All (fun x : def termtest_def (on_free_vars xpredT) (on_free_vars (shiftnP #|mfix| xpredT)) x) mfix
  on_ctx_free_vars xpredT Γ
  on_ctx_free_vars xpredT (Γ,,, fix_context mfix).
Proof.
  intros.
  rewrite -(shiftnP_xpredT #|mfix|).
  apply on_ctx_free_vars_fix_context ⇒ //.
Qed.

Lemma on_free_vars_ctx_fix_context_xpredT (Γ : list context_decl) mfix :
  All (fun x : def termtest_def (on_free_vars xpredT) (on_free_vars (shiftnP #|mfix| xpredT)) x) mfix
  on_free_vars_ctx xpredT Γ
  on_free_vars_ctx xpredT (Γ,,, fix_context mfix).
Proof.
  intros.
  rewrite on_free_vars_ctx_app shiftnP_xpredT.
  rewrite H on_free_vars_fix_context //.
Qed.

Lemma pred_on_free_vars {cf : checker_flags} {Σ} {wfΣ : wf Σ} {P Γ Δ t u} :
  on_ctx_free_vars P Γ
  clos_refl_trans (pred1 Σ Γ Δ) t u
  on_free_vars P t on_free_vars P u.
Proof.
  intros onΓ.
  induction 1; eauto with fvs. intros o.
  eapply pred1_on_free_vars; tea.
Qed.

Ltac inv_on_free_vars_xpredT :=
  match goal with
  | [ H : is_true (on_free_vars (shiftnP _ _) _) |- _ ] ⇒
    rewriteshiftnP_xpredT in H
  | [ H : is_true (_ && _) |- _ ] ⇒
    move/andP: H ⇒ []; intros
  | [ 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
  | [ H : is_true (test_def (on_free_vars ?P) ?Q ?x) |- _ ] ⇒
    let H0 := fresh in let H' := fresh in
    move/andP: H ⇒ [H0 H'];
    try rewriteshiftnP_xpredT in H0;
    try rewriteshiftnP_xpredT in H';
    intros
  | [ H : is_true (test_context_k _ _ _ ) |- _ ] ⇒
    rewritetest_context_k_closed_on_free_vars_ctx in H
  end.
#[global] Hint Resolve on_free_vars_ctx_closed_xpredT : fvs.

#[global] Hint Resolve red1_on_free_vars red_on_free_vars : fvs.
#[global] Hint Resolve pred1_on_free_vars pred1_on_ctx_free_vars : fvs.
#[global] Hint Extern 4 ⇒ progress (unfold PCUICCases.inst_case_predicate_context) : fvs.
#[global] Hint Extern 4 ⇒ progress (unfold PCUICCases.inst_case_branch_context) : fvs.
#[global] Hint Extern 3 (is_true (on_ctx_free_vars xpredT _)) ⇒
  rewrite on_ctx_free_vars_xpredT_snoc : fvs.
#[global] Hint Extern 3 (is_true (on_free_vars_ctx (shiftnP _ xpredT) _)) ⇒
  rewrite shiftnP_xpredT : fvs.
#[global] Hint Resolve on_ctx_free_vars_inst_case_context_xpredT : fvs.
#[global] Hint Resolve on_ctx_free_vars_fix_context_xpredT : fvs.
#[global] Hint Resolve on_free_vars_ctx_fix_context_xpredT : fvs.
#[global] Hint Resolve on_free_vars_ctx_inst_case_context_xpredT : fvs.
#[global] Hint Extern 3 (is_true (on_free_vars (shiftnP _ xpredT) _)) ⇒ rewrite shiftnP_xpredT : fvs.

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

  Hint Resolve pred1_ctx_over_refl : pcuic.
  Hint Unfold All2_prop2_eq : pcuic.
  Hint Transparent context : pcuic.
  Hint Transparent mfixpoint : pcuic.

  Hint Mode pred1 ! ! ! ! - : pcuic.

  Ltac pcuic := simpl; try typeclasses eauto with pcuic.

Strong substitutivity gives context conversion of reduction! It cannot be strenghtened to deal with let-ins: pred1 is precisely not closed by arbitrary reductions in contexts with let-ins.

  Lemma pred1_ctx_pred1 P Γ Γ' Δ Δ' t u :
    #|Γ| = #|Γ'|
    on_free_vars (closedP #|Γ ,,, Δ| P) t
    on_ctx_free_vars (closedP #|Γ ,,, Δ| P) (Γ ,,, Δ)
    pred1 Σ (Γ ,,, Δ) (Γ' ,,, Δ) t u
    assumption_context Δ
    pred1_ctx Σ (Γ ,,, Δ) (Γ' ,,, Δ')
    pred1 Σ (Γ ,,, Δ) (Γ' ,,, Δ') t u.
  Proof using wfΣ.
    intros Hlen ont onctx X H X0.
    epose proof (fst strong_substitutivity _ _ _ _ X _ _ (Γ ,,, Δ) (Γ' ,,, Δ') ids ids ont).
    forward X1. now rewrite subst_ids.
    rewrite !subst_ids in X1.
    apply X1.
    red. split ⇒ //. split ⇒ //.
    intros x px. rewrite {1}/ids /=. split ⇒ //.
    split ⇒ //. eapply pred1_refl_gen ⇒ //.
    move⇒ [na [b|] ty] ⇒ /= //.
    destruct (leb_spec_Set (S x) #|Δ|).
    rewrite !nth_error_app_lt; try lia.
    intros hnth; rewrite hnth. eexists; split ⇒ //.
    apply nth_error_assumption_context in hnth ⇒ //.
    rewrite !nth_error_app_ge //; try lia.
    intros hnth.
    pose proof (on_contexts_app_inv _ _ _ _ _ X0) as [predΓ _] ⇒ //.
    pose proof (All2_fold_length X0). len in H0.
    eapply nth_error_pred1_ctx_l in predΓ; tea.
    2:erewrite hnth ⇒ //.
    destruct predΓ as [body' [hnth' pred]].
     body'; split⇒ //.
    rewrite -lift0_inst /ids /=.
    econstructor ⇒ //.
    rewrite nth_error_app_ge. lia.
    now replace #|Δ'| with #|Δ| by lia.
  Qed.

  Lemma pred1_ctx_assumption_context Γ Γ' :
    pred1_ctx Σ Γ Γ'
    assumption_context Γ assumption_context Γ'.
  Proof using Type.
    induction 1; auto.
    intros h; depelim h. depelim p; constructor; auto.
  Qed.

  Lemma pred1_ctx_over_assumption_context Γ Γ' Δ Δ' :
    pred1_ctx_over Σ Γ Γ' Δ Δ'
    assumption_context Δ assumption_context Δ'.
  Proof using Type.
    induction 1; auto.
    intros h; depelim h. depelim p; constructor; auto.
  Qed.

  Lemma pred1_ctx_pred1_inv P Γ Γ' Δ Δ' t u :
    #|Γ| = #|Γ'|
    on_free_vars (closedP #|Γ ,,, Δ| P) t
    on_ctx_free_vars (closedP #|Γ ,,, Δ| P) (Γ ,,, Δ)
    pred1 Σ (Γ ,,, Δ) (Γ' ,,, Δ') t u
    assumption_context Δ
    pred1 Σ (Γ ,,, Δ) (Γ' ,,, Δ) t u.
  Proof using wfΣ.
    intros Hlen ont onctx X H.
    assert(pred1_ctx Σ (Γ ,,, Δ) (Γ' ,,, Δ)).
    { apply pred1_pred1_ctx in X.
      apply on_contexts_app_inv in X as [] ⇒ //.
      apply All2_fold_app ⇒ //. now eapply pred1_ctx_over_refl_gen. }
    assert(lenΔ : #|Δ| = #|Δ'|).
    { eapply pred1_pred1_ctx in X. eapply All2_fold_length in X.
      rewrite !app_context_length in X. lia. }
    epose proof (fst strong_substitutivity _ _ _ _ X _ _ (Γ ,,, Δ) (Γ' ,,, Δ) ids ids ont).
    forward X1. now rewrite subst_ids.
    rewrite !subst_ids in X1.
    apply X1; red; split ⇒ //; split ⇒ //.
    intros x px. rewrite {1}/ids /=. split ⇒ //.
    split ⇒ //. eapply pred1_refl_gen ⇒ //.
    move⇒ [na [b|] ty] ⇒ /= //.
    destruct (leb_spec_Set (S x) #|Δ|).
    rewrite !nth_error_app_lt; try lia.
    intros hnth.
    apply nth_error_assumption_context in hnth ⇒ //.
    rewrite !nth_error_app_ge //; try lia.
    intros hnth.
    pose proof (on_contexts_app_inv _ _ _ _ _ X0) as [predΓ _] ⇒ //.
    pose proof (All2_fold_length X0). len in H0.
    eapply nth_error_pred1_ctx_l in predΓ; tea.
    2:erewrite hnth ⇒ //.
    destruct predΓ as [body' [hnth' pred]].
    replace #|Δ'| with #|Δ| by lia.
     body'; split⇒ //.
    rewrite -lift0_inst /ids /=.
    econstructor ⇒ //.
    rewrite nth_error_app_ge //. lia.
  Qed.

  Ltac noconf H := repeat (DepElim.noconf H; simpl NoConfusion in × ).

  Hint Extern 1 (eq_binder_annot _ _) ⇒ reflexivity : pcuic.
  Hint Resolve pred1_refl_gen : pcuic.
  Hint Extern 4 (All_decls _ _ _) ⇒ constructor : pcuic.
  Hint Extern 4 (All2_fold _ _ _) ⇒ constructor : pcuic.

  Lemma OnOne2_local_env_pred1_ctx_over Γ Δ Δ' :
     OnOne2_local_env (on_one_decl (fun Δ M Npred1 Σ (Γ ,,, Δ) (Γ ,,, Δ) M N)) Δ Δ'
     pred1_ctx_over Σ Γ Γ Δ Δ'.
  Proof using Type.
    induction 1.
    1-2:constructor; destruct p; subst; intuition eauto.
    - eapply pred1_pred1_ctx in p. pcuic.
    - now constructor.
    - eapply pred1_pred1_ctx in a0. pcuic.
    - eapply pred1_pred1_ctx in a. pcuic.
    - constructor; simpl; subst; intuition auto.
      eapply pred1_refl.
    - constructor; simpl; subst; intuition auto.
      eapply pred1_refl.
    - eapply (All2_fold_app (Γ' := [d]) (Γr := [_])); pcuic.
      destruct d as [na [b|] ty]; constructor; pcuic.
      constructor; simpl; subst; auto; intuition pcuic.
      eapply pred1_refl_gen. eapply All2_fold_app; pcuic. apply IHX.
      eapply pred1_refl_gen. eapply All2_fold_app; pcuic. apply IHX.
      simpl; subst; intuition pcuic.
      constructor.
      eapply pred1_refl_gen. eapply All2_fold_app; pcuic. apply IHX.
  Qed.

  Lemma prod_ind {A B} : A (A B) A × B.
  Proof using Type.
    intuition.
  Qed.

  Lemma red1_pred1 Γ M N :
    on_ctx_free_vars xpredT Γ
    on_free_vars xpredT M
    red1 Σ Γ M N pred1 Σ Γ Γ M N.
  Proof using wfΣ with pcuic.
    intros onΓ onM r.
    induction r using red1_ind_all; intros; pcuic.
    all:repeat inv_on_free_vars_xpredT.
    all:try solve [econstructor; pcuic;
      (eapply All_All2_refl, All_refl || eapply OnOne2_All2 || idtac); eauto 7 using pred1_refl, pred1_ctx_over_refl with fvs ].
    - eapply OnOne2_prod_inv in X as [].
      eapply OnOne2_apply in o0 ⇒ //.
      eapply OnOne2_apply_All in o0 ⇒ //. 2:solve_all.
      assert (pred1_ctx_over Σ Γ Γ (PCUICCases.inst_case_predicate_context p)
        (PCUICCases.inst_case_predicate_context (set_pparams p params'))).
      eapply OnOne2_pars_pred1_ctx_over ⇒ //. eauto with fvs.
      econstructor; pcuic; eauto 6 with fvs.
      eapply OnOne2_All2...
      eapply pred1_refl_gen. eapply All2_fold_app ⇒ //; pcuic.
      eapply All_All2_refl; solve_all; repeat inv_on_free_vars_xpredT.
      eapply OnOne2_pars_pred1_ctx_over ⇒ //; eauto with fvs; solve_all.
      eapply pred1_refl_gen. eapply All2_fold_app ⇒ //; pcuic.
      eapply OnOne2_pars_pred1_ctx_over ⇒ //; eauto with fvs; solve_all.
    - econstructor; pcuic. solve_all.
      unfold inst_case_branch_context in ×.
      eapply OnOne2_All_mix_left in X; tea.
      eapply OnOne2_All2...
      simpl. intros x y [[[? ?] ?]]; unfold on_Trel; intuition pcuic;
        rewrite -?e; solve_all; repeat inv_on_free_vars_xpredT; eauto with fvs.
      eapply pred1_ctx_over_refl. eapply p5; eauto with fvs.
      eapply on_ctx_free_vars_inst_case_context_xpredT ⇒ //; eauto with fvs. solve_all.
    - constructor; pcuic.
      eapply OnOne2_prod_inv in X as [].
      eapply OnOne2_apply in o0 ⇒ //.
      eapply OnOne2_apply_All in o0 ⇒ //.
      eapply OnOne2_All2...
    - assert (pred1_ctx_over Σ Γ Γ (fix_context mfix0) (fix_context mfix1)).
      { eapply pred1_fix_context; tea. solve_all. pcuic.
        eapply OnOne2_prod_assoc in X as [].
        eapply OnOne2_All_mix_left in o0; tea.
        eapply OnOne2_All2...
        intros.
        simpl in ×. intuition auto. noconf b0. inv_on_free_vars_xpredT; eauto with fvs.
        now noconf b0. }
      constructor; pcuic.
      eapply OnOne2_prod_assoc in X as [].
      eapply OnOne2_All_mix_left in o0; tea.
      eapply OnOne2_All2; pcuic; simpl;
        unfold on_Trel; simpl; intros; intuition auto; noconf b0; try inv_on_free_vars_xpredT; eauto with fvs.
        rewrite H0. eapply pred1_refl_gen ⇒ //.
        eapply All2_fold_app; pcuic. apply X0. congruence.
        eapply pred1_refl.
        apply pred1_refl_gen ⇒ //.
        eapply All2_fold_app; pcuic. apply X0.

    - assert (fix_context mfix0 = fix_context mfix1).
      { clear -X.
        unfold fix_context, mapi. generalize 0 at 2 4.
        induction X; intros. intuition auto. simpl.
        noconf b; noconf H. now rewrite H H0.
        simpl; now rewrite IHX. }
      assert(pred1_ctx_over Σ Γ Γ (fix_context mfix0) (fix_context mfix0)).
      { rewrite H. apply pred1_ctx_over_refl. }
      constructor; pcuic.
      now rewrite -H.
      eapply OnOne2_prod_assoc in X as [].
      eapply OnOne2_All_mix_left in o0; tea.
      eapply OnOne2_All2; pcuic; simpl;
        unfold on_Trel; simpl; intros; intuition auto; noconf b0; repeat inv_on_free_vars_xpredT; eauto with fvs.
      rewrite H1. eapply pred1_refl.
      rewrite -H. eapply a0; eauto with fvs. congruence.
      eapply pred1_refl.
      apply pred1_refl_gen ⇒ //.
      now rewrite -H; pcuic.

    - assert (pred1_ctx_over Σ Γ Γ (fix_context mfix0) (fix_context mfix1)).
      { eapply pred1_fix_context; tea. solve_all. pcuic.
        eapply OnOne2_prod_assoc in X as [].
        eapply OnOne2_All_mix_left in o0; tea.
        eapply OnOne2_All2...
        intros.
        simpl in ×. intuition auto. noconf b0. inv_on_free_vars_xpredT; eauto with fvs.
        now noconf b0. }
      constructor; pcuic.
      eapply OnOne2_prod_assoc in X as [].
      eapply OnOne2_All_mix_left in o0; tea.
      eapply OnOne2_All2; pcuic; simpl;
        unfold on_Trel; simpl; intros; intuition auto; noconf b0; try inv_on_free_vars_xpredT; eauto with fvs.
        rewrite H0. eapply pred1_refl_gen ⇒ //.
        eapply All2_fold_app; pcuic; tas. congruence.
        eapply pred1_refl.
        apply pred1_refl_gen ⇒ //.
        eapply All2_fold_app; pcuic; tas.

    - assert (fix_context mfix0 = fix_context mfix1).
      { clear -X.
        unfold fix_context, mapi. generalize 0 at 2 4.
        induction X; intros. intuition auto. simpl.
        noconf b; noconf H. now rewrite H H0.
        simpl; now rewrite IHX. }
      assert(pred1_ctx_over Σ Γ Γ (fix_context mfix0) (fix_context mfix0)).
      { rewrite H. apply pred1_ctx_over_refl. }
      constructor; pcuic.
      now rewrite -H.
      eapply OnOne2_prod_assoc in X as [].
      eapply OnOne2_All_mix_left in o0; tea.
      eapply OnOne2_All2; pcuic; simpl;
        unfold on_Trel; simpl; intros; intuition auto; noconf b0; repeat inv_on_free_vars_xpredT; eauto with fvs.
      rewrite H1. eapply pred1_refl.
      rewrite -H. eapply a0; eauto with fvs. congruence.
      eapply pred1_refl.
      apply pred1_refl_gen ⇒ //.
      now rewrite -H; pcuic.
  Qed.

End RedPred.

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

Parallel reduction is included in the reflexive transitive closure of 1-step reduction
  Lemma pred1_red Γ Γ' : M N, pred1 Σ Γ Γ' M N
    on_free_vars_ctx xpredT Γ
    on_free_vars xpredT M
    red Σ Γ M N.
  Proof using cf Σ wfΣ.
    revert Γ Γ'. eapply (@pred1_ind_all_ctx Σ
      (fun Γ Γ' M Non_free_vars_ctx xpredT Γ on_free_vars xpredT M red Σ Γ M N)
      (fun Γ Γ'on_free_vars_ctx xpredT Γ All2_fold (on_decls (fun Γ Γ' M Nred Σ Γ M N)) Γ Γ')%type
      (fun Γ Γ' Δ Δ'on_free_vars_ctx xpredT (Γ ,,, Δ) on_contexts_over (fun Γ Γ' M Nred Σ Γ M N) Γ Γ' Δ Δ')%type);
      intros; try reflexivity; repeat inv_on_free_vars_xpredT; try solve [pcuic].

    -
      eapply on_free_vars_ctx_All_fold in H.
      eapply All2_fold_All_fold_mix_left in X0; tea.
      eapply All2_fold_impl_ind. exact X0.
      intros ???? IH IH' [].
      eapply All2_fold_prod_inv in IH as [].
      eapply All2_fold_All_left in a0.
      apply on_free_vars_ctx_All_fold in a0.
      eapply All_decls_on_free_vars_impl; tea.
      cbn; intros ?? ont IH. inv_on_free_vars_xpredT; eauto.

    -
      move: H.
      rewrite on_free_vars_ctx_app ⇒ /andP[] onΓ onΔ.
      setoid_rewrite shiftnP_xpredT in onΔ.
      intuition auto.
      eapply on_free_vars_ctx_All_fold in onΔ.
      eapply All2_fold_All_fold_mix_left in X3; tea.
      eapply All2_fold_impl_ind. exact X3.
      intros ???? IH IH' [].
      eapply All2_fold_prod_inv in IH as [].
      eapply All2_fold_All_left in a0.
      apply on_free_vars_ctx_All_fold in a0.
      eapply All_decls_on_free_vars_impl; tea.
      cbn; intros ?? ont IH.
      inv_on_free_vars_xpredT; eauto. eauto 6 with fvs.

    -
      intuition auto.
      apply red_trans with (tApp (tLambda na t0 b1) a0).
      eapply (@red_app Σ); [apply red_abs|]; eauto with pcuic fvs.
      apply red_trans with (tApp (tLambda na t0 b1) a1).
      eapply (@red_app Σ); auto with pcuic.
      apply red1_red. constructor.

    -
      eapply red_trans with (tLetIn na d0 t0 b1).
      eapply red_letin; eauto 6 with pcuic fvs.
      eapply red_trans with (tLetIn na d1 t1 b1).
      eapply red_letin; eauto with pcuic.
      eapply red1_red; constructor.

    -
      eapply nth_error_pred1_ctx in X0; eauto.
      destruct X0 as [body' [Hnth Hpred]].
      eapply red_trans with (lift0 (S i) body').
      eapply red1_red; constructor; auto.
      eapply nth_error_pred1_ctx_all_defs in H; eauto.
      rewrite -(firstn_skipn (S i) Γ).
      eapply weakening_red_0 ⇒ //.
      rewrite firstn_length_le //.
      destruct nth_error eqn:Heq.
      eapply nth_error_Some_length in Heq. lia. noconf Hnth.
      erewrite on_free_vars_ctx_on_ctx_free_vars.
      move: H0; rewrite -{1}(firstn_skipn (S i) Γ) on_free_vars_ctx_app ⇒ /andP[] onΓ _.
      exact onΓ. eauto with fvs.
      destruct (nth_error Γ i) eqn:hnth ⇒ //. cbn in Hnth. noconf Hnth.
      destruct c as [na [b|] ty] ⇒ //. noconf H.
      rewrite <- on_free_vars_ctx_on_ctx_free_vars in H0.
      setoid_rewrite shiftnP_xpredT in H0.
      move/alli_Alli: H0H0.
      eapply nth_error_alli in H0; tea.
      cbn in H0. rewriteaddnP_xpredT in H0.
      move/andP: H0 ⇒ /= []. eauto with fvs.

    -
      transitivity (tCase ci p0 (mkApps (tConstruct ci.(ci_ind) c u) args1) brs1).
      etransitivity.
      { eapply red_case_c. eapply red_mkApps. auto. solve_all. }
      etransitivity.
      { eapply red_case_brs. red. solve_all;
        unfold on_Trel in *; intuition auto; repeat inv_on_free_vars_xpredT.
        eapply b0; eauto with fvs.
        rewrite -on_free_vars_ctx_on_ctx_free_vars. len.
        rewrite shiftnP_xpredT.
        eapply on_ctx_free_vars_inst_case_context_xpredT; eauto with fvs. solve_all.
        eapply on_free_vars_ctx_on_ctx_free_vars_xpredT; tea. }
      reflexivity.
      transitivity (tCase ci (set_pparams p0 pparams1) (mkApps (tConstruct ci.(ci_ind) c u) args1) brs1).
      { eapply red_case_pars. solve_all. }
      eapply red1_red. constructor ⇒ //.

    - move: H H0.
      moveunf isc.
      transitivity (mkApps (tFix mfix1 idx) args1).
      assert (on_ctx_free_vars xpredT (Γ,,, fix_context mfix0)).
      { eapply on_ctx_free_vars_fix_context_xpredT; eauto with fvs.
        now eapply on_free_vars_ctx_on_ctx_free_vars_xpredT. }
      eapply red_mkApps. eapply red_fix_congr. red in X3.
      eapply All2_All_mix_left in X3; tea.
      eapply (All2_impl X3); unfold on_Trel in *; intuition auto; repeat inv_on_free_vars_xpredT; auto.
      eapply b1; eauto with fvs. solve_all.
      eapply red_step. econstructor; eauto. 2:eauto.
      eapply (is_constructor_pred1 Σ); eauto. eapply (All2_impl X4); intuition eauto.

    - transitivity (tCase ci p1 (mkApps (tCoFix mfix1 idx) args1) brs1).
      destruct p1; unfold on_Trel in *; cbn in ×.
      subst puinst. subst pcontext.
      eapply red_case; eauto.
      × solve_all.
      × eapply X8; eauto with fvs.
      × eapply red_mkApps; [|solve_all].
        etransitivity. eapply red_cofix_congr.
        eapply All2_All_mix_left in X3; tea.
        eapply (All2_impl X3); unfold on_Trel; intuition auto; repeat inv_on_free_vars_xpredT; eauto with fvs.
        reflexivity.
      × red. eapply forallb_All in p5.
        eapply All2_All_mix_left in X9; tea.
        eapply (All2_impl X9); unfold on_Trel; intuition auto;
          repeat inv_on_free_vars_xpredT; eauto with fvs.
      × constructor. econstructor; eauto.

    - transitivity (tProj p (mkApps (tCoFix mfix1 idx) args1)).
      eapply red_proj_c; eauto.
      cbn in H1. repeat inv_on_free_vars_xpredT.
      eapply red_mkApps; [|solve_all].
      eapply red_cofix_congr.
      eapply All2_All_mix_left in X3; tea.
      eapply (All2_impl X3); unfold on_Trel; intuition auto; repeat inv_on_free_vars_xpredT; eauto with fvs.
      eapply red_step. econstructor; eauto. eauto.

    - transitivity (tProj p (mkApps (tConstruct p.(proj_ind) 0 u) args1)).
      eapply red_proj_c; eauto.
      cbn in H1. repeat inv_on_free_vars_xpredT.
      eapply red_mkApps; [|solve_all]. auto.
      eapply red1_red. econstructor; eauto.

    - eapply PCUICSubstitution.red_abs_alt; eauto with fvs.
    - now eapply red_app.
    - now eapply PCUICSubstitution.red_letin_alt ⇒ //; eauto with fvs.
    - unfold on_Trel in *; destruct p1; cbn in ×. subst puinst pcontext.
      eapply red_case ⇒ //.
      × solve_all.
      × eapply X4; eauto with fvs.
      × eauto.
      × eapply forallb_All in p5.
        red. eapply All2_All_mix_left in X5; tea.
        eapply (All2_impl X5); unfold on_Trel; intuition auto; repeat inv_on_free_vars_xpredT; eauto with fvs.

    - now eapply red_proj_c.
    - eapply red_fix_congr.
      eapply All2_All_mix_left in X3; tea.
      eapply (All2_impl X3); unfold on_Trel; intuition auto; repeat inv_on_free_vars_xpredT; eauto with fvs.
    - eapply red_cofix_congr.
      eapply All2_All_mix_left in X3; tea.
      eapply (All2_impl X3); unfold on_Trel; intuition auto; repeat inv_on_free_vars_xpredT; eauto with fvs.
    - eapply red_prod; eauto with fvs.
    - eapply red_evar; eauto with fvs. solve_all.
  Qed.

  Lemma pred1_red_r_gen P Γ Γ' Δ Δ' : M N,
    on_free_vars (closedP #|Γ ,,, Δ| P) M
    on_ctx_free_vars (closedP #|Γ ,,, Δ| P) (Γ' ,,, Δ)
    pred1 Σ (Γ ,,, Δ) (Γ' ,,, Δ') M N
    #|Γ| = #|Γ'|
    pred1_ctx Σ (Γ' ,,, Δ) (Γ' ,,, Δ')
    pred1 Σ (Γ' ,,, Δ) (Γ' ,,, Δ') M N.
  Proof using wfΣ.
    intros M N onM onctx pred hlen predctx.
    epose proof (fst strong_substitutivity _ _ _ _ pred _ _ (Γ' ,,, Δ) (Γ' ,,, Δ') ids ids onM).
    forward X. now rewrite subst_ids.
    rewrite !subst_ids in X.
    apply X.
    red. split ⇒ //. split ⇒ //.
    intros x px. rewrite {1}/ids /=. split ⇒ //.
    split ⇒ //. eapply pred1_refl_gen ⇒ //.
    assert (#|Δ| = #|Δ'|).
    { apply pred1_pred1_ctx in pred. eapply All2_fold_length in pred. len in pred. }
    move⇒ [na [b|] ty] ⇒ /= //.
    destruct (leb_spec_Set (S x) #|Δ|).
    - rewrite !nth_error_app_lt; try lia.
      intros hnth.
      destruct (on_contexts_app_inv _ _ _ _ _ predctx) as []. lia.
      eapply nth_error_pred1_ctx_l in a0; tea.
      2:erewrite hnth; rewrite /= //.
      destruct a0 as [body' [heq hpred]]. body'; split ⇒ //.
      rewrite -lift0_inst /ids.
      econstructor; eauto.
      rewrite nth_error_app_lt //; try lia.
    - rewrite !nth_error_app_ge //; try lia.
      intros hnth.
      pose proof (on_contexts_app_inv _ _ _ _ _ (pred1_pred1_ctx _ pred)) as [predΓ _] ⇒ //.
      eapply nth_error_pred1_ctx_l in predΓ; tea.
      2:erewrite hnth ⇒ //.
      destruct predΓ as [body' [hnth' pred']].
      rewrite -H.
       body'; split⇒ //.
      rewrite -lift0_inst /ids /=.
      econstructor ⇒ //.
      rewrite nth_error_app_ge. lia.
      now replace #|Δ'| with #|Δ| by lia.
  Qed.

  Lemma pred1_red_r_gen' P Γ Γ' Δ Δ' : M N,
    on_free_vars (shiftnP #|Γ ,,, Δ| P) M
    on_free_vars_ctx P (Γ' ,,, Δ)
    pred1 Σ (Γ ,,, Δ) (Γ' ,,, Δ') M N
    #|Γ| = #|Γ'|
    pred1_ctx Σ (Γ' ,,, Δ) (Γ' ,,, Δ')
    pred1 Σ (Γ' ,,, Δ) (Γ' ,,, Δ') M N.
  Proof using wfΣ.
    intros M N onM onctx pred hlen predctx.
    epose proof (fst strong_substitutivity _ _ _ _ pred _ _ (Γ' ,,, Δ) (Γ' ,,, Δ') ids ids onM).
    forward X. now rewrite subst_ids.
    rewrite !subst_ids in X.
    apply X.
    pose proof (All2_fold_length predctx). len in H.
    red. split ⇒ //. split ⇒ //.
    relativize #|Γ ,,, Δ|; [erewrite on_free_vars_ctx_on_ctx_free_vars|] ⇒ //; len.
    intros x px. rewrite {1}/ids /=. split ⇒ //.
    split ⇒ //. eapply pred1_refl_gen ⇒ //.
    assert (#|Δ| = #|Δ'|).
    { apply pred1_pred1_ctx in pred. eapply All2_fold_length in pred. len in pred. }
    move⇒ [na [b|] ty] ⇒ /= //.
    destruct (leb_spec_Set (S x) #|Δ|).
    - rewrite !nth_error_app_lt; try lia.
      intros hnth.
      destruct (on_contexts_app_inv _ _ _ _ _ predctx) as []. lia.
      eapply nth_error_pred1_ctx_l in a0; tea.
      2:erewrite hnth; rewrite /= //.
      destruct a0 as [body' [heq hpred]]. body'; split ⇒ //.
      rewrite -lift0_inst /ids.
      econstructor; eauto.
      rewrite nth_error_app_lt //; try lia.
    - rewrite !nth_error_app_ge //; try lia.
      intros hnth.
      pose proof (on_contexts_app_inv _ _ _ _ _ (pred1_pred1_ctx _ pred)) as [predΓ _] ⇒ //.
      eapply nth_error_pred1_ctx_l in predΓ; tea.
      2:erewrite hnth ⇒ //.
      destruct predΓ as [body' [hnth' pred']].
      rewrite -H0.
       body'; split⇒ //.
      rewrite -lift0_inst /ids /=.
      econstructor ⇒ //.
      rewrite nth_error_app_ge. lia.
      now replace #|Δ'| with #|Δ| by lia.
  Qed.

  Lemma pred1_pred1_r P Γ Γ' : M N, pred1 Σ Γ Γ' M N
    on_ctx_free_vars (closedP #|Γ| P) Γ'
    on_free_vars (closedP #|Γ| P) M
    pred1 Σ Γ' Γ' M N.
  Proof using wfΣ.
    intros M N pred onctx onM.
    apply (pred1_red_r_gen P _ _ [] [] M N onM onctx pred).
    eapply pred1_pred1_ctx in pred. apply (length_of pred).
    simpl. eapply pred1_ctx_refl.
  Qed.

  Lemma pred1_pred1_r' P Γ Γ' : M N, pred1 Σ Γ Γ' M N
    on_free_vars_ctx P Γ'
    on_free_vars (shiftnP #|Γ| P) M
    pred1 Σ Γ' Γ' M N.
  Proof using wfΣ.
    intros M N pred onctx onM.
    apply (pred1_red_r_gen' P _ _ [] [] M N onM onctx pred).
    eapply pred1_pred1_ctx in pred. apply (length_of pred).
    simpl. eapply pred1_ctx_refl.
  Qed.

  Lemma pred1_red_r {P Γ Γ' M N} :
    pred1 Σ Γ Γ' M N
    on_free_vars_ctx P Γ'
    on_free_vars (shiftnP #|Γ| P) M
    red Σ Γ' M N.
  Proof using wfΣ.
    intros p onctx onM.
    pose proof (pred1_pred1_ctx _ p). eapply All2_fold_length in X.
    eapply pred1_pred1_r' in p; tea.
    eapply pred1_red in p; tea.
    eapply on_free_vars_ctx_impl; tea ⇒ //.
    eapply on_free_vars_impl; tea ⇒ //.
  Qed.

End PredRed.

#[global] Hint Resolve on_free_vars_ctx_any_xpredT : fvs.

#[global] Hint Extern 4 (is_true (on_ctx_free_vars xpredT _)) ⇒
  rewrite on_ctx_free_vars_xpredT : fvs.

Lemma on_free_vars_any_xpredT P t : on_free_vars P t on_free_vars xpredT t.
Proof.
  apply on_free_vars_impl ⇒ //.
Qed.
#[global] Hint Resolve on_free_vars_any_xpredT : fvs.

Generalizable Variables A B R S.

Section AbstractConfluence.
  Section Definitions.

    Context {A : Type}.
    Definition joinable (R : A A Type) (x y : A) := z, R x z × R y z.
    Definition diamond (R : A A Type) := x y z, R x y R x z joinable R y z.
    Definition confluent (R : relation A) := diamond (clos_refl_trans R).

  End Definitions.

  Global Instance joinable_proper A :
    Proper (relation_equivalence ==> relation_equivalence)%signatureT (@joinable A).
  Proof.
    reduce_goal. split; unfold joinable; intros.
    destruct X0. x1. intuition eauto. setoid_rewrite (X x0 x1) in a. auto.
    specialize (X y0 x1). now apply X in b.
    red in X.
    destruct X0 as [z [rl rr]].
    apply X in rl. apply X in rr.
     z; split; auto.
  Qed.

  Global Instance diamond_proper A : Proper (relation_equivalence ==> iffT)%signatureT (@diamond A).
  Proof.
    reduce_goal.
    rewrite /diamond.
    split; intros.
    setoid_rewrite <- (X x0 y0) in X1.
    setoid_rewrite <- (X x0 z) in X2.
    specialize (X0 _ _ _ X1 X2).
    pose (joinable_proper _ _ _ X).
    now apply r in X0.
    setoid_rewrite (X x0 y0) in X1.
    setoid_rewrite (X x0 z) in X2.
    specialize (X0 _ _ _ X1 X2).
    pose (joinable_proper _ _ _ X).
    now apply r in X0.
  Qed.

  Lemma clos_rt_proper A : Proper (relation_equivalence ==> relation_equivalence) (@clos_refl_trans A).
  Proof.
    reduce_goal. split; intros.
    induction X0; try apply X in r; try solve [econstructor; eauto].
    induction X0; try apply X in r; try solve [econstructor; eauto].
  Qed.

  Global Instance confluent_proper A : Proper (relation_equivalence ==> iffT)%signatureT (@confluent A).
  Proof.
    reduce_goal.
    split; rewrite /confluent; auto.
    pose proof (diamond_proper A). apply X0. apply clos_rt_proper.
    now symmetry.
    pose proof (diamond_proper A). apply X0. apply clos_rt_proper.
    now symmetry.
  Qed.

  Lemma sandwich {A} (R S : A A Type) :
    inclusion R S inclusion S (clos_refl_trans R)
    (iffT (confluent S) (confluent R)).
  Proof.
    intros inclR inclS.
    apply clos_rt_monotone in inclR.
    apply clos_rt_monotone in inclS.
    assert (inclusion (clos_refl_trans S) (clos_refl_trans R)).
    etransitivity; eauto.
    apply clos_rt_idempotent.
    rewrite /confluent.
    apply diamond_proper.
    now apply relation_equivalence_inclusion.
  Qed.

  Section Diamond.
    Context {A} {R S : relation A}.
    Context (sc : diamond R).

    Lemma diamond_t1n_t_confluent t u v :
      trans_clos_1n R t u
      R t v
       t', trans_clos_1n R u t' × trans_clos_1n R v t'.
    Proof using sc.
      movetu.