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 y ⇒ P 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 y ⇒ Q 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 y ⇒ Q 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 y ⇒ P (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 y ⇒ B Γ x y → P Γ x y)) l l' →
  OnOne2_local_env (on_one_decl (fun Γ x y ⇒ P Γ 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 y ⇒ P 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 y ⇒ on_Trel_eq (red1 Σ (Δ ,,, inst_case_branch_context p x)) bbody bcontext x y)
      (fun x y ⇒ on_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 : nat ⇒ lift0 n)
                   (Γ ,,, Δ) (Γ' ,,, Δ') #|Δ|
    (map (fun def : def term ⇒ vass (dname def) (dtype def)) m)
    (map (fun def : def term ⇒ vass (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 n ⇒ lift0 n)
                   Γ Γ' 0
                   (map (fun def ⇒ vass (dname def) (dtype def)) m)
                   (map (fun def ⇒ vass (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 def ⇒ vass (dname def) (dtype def))
                (fun n decl ⇒ lift_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 term ⇒ test_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 term ⇒ test_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 _ _) _) |- _ ] ⇒
    rewrite → shiftnP_xpredT in H
  | [ H : is_true (_ && _) |- _ ] ⇒
    move/andP: H ⇒ []; intros
  | [ H : is_true (on_free_vars ?P ?t) |- _ ] ⇒
    progress (cbn in H || rewrite → on_free_vars_mkApps in H);
    (move/and5P: H ⇒ [] || move/and4P: H ⇒ [] || move/and3P: H ⇒ [] || move/andP: H ⇒ [] ||
      eapply forallb_All in H); intros
  | [ H : is_true (test_def (on_free_vars ?P) ?Q ?x) |- _ ] ⇒
    let H0 := fresh in let H' := fresh in
    move/andP: H ⇒ [H0 H'];
    try rewrite → shiftnP_xpredT in H0;
    try rewrite → shiftnP_xpredT in H';
    intros
  | [ H : is_true (test_context_k _ _ _ ) |- _ ] ⇒
    rewrite → test_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.