Library MetaCoq.SafeChecker.PCUICSafeConversion

From Coq Require Import ProofIrrelevance.
From MetaCoq.Template Require Import config utils uGraph.
From MetaCoq.PCUIC Require Import PCUICAst PCUICAstUtils
     PCUICReflect PCUICLiftSubst PCUICUnivSubst PCUICTyping PCUICGlobalEnv
     PCUICCumulativity PCUICConversion PCUICEquality PCUICConversion
     PCUICSafeLemmata PCUICNormal PCUICInversion PCUICReduction PCUICPosition
     PCUICPrincipality PCUICContextConversion PCUICContextConversionTyp PCUICSN PCUICUtils PCUICWfUniverses
     PCUICOnFreeVars PCUICWellScopedCumulativity
     PCUICWeakeningEnvConv PCUICWeakeningEnvTyp
     PCUICWeakeningConv PCUICWeakeningTyp
     PCUICClosed PCUICClosedTyp PCUICConvCumInversion .
From MetaCoq.SafeChecker Require Import PCUICErrors PCUICWfEnv PCUICSafeReduce PCUICEqualityDec.

Require Import Equations.Prop.DepElim.
From Equations Require Import Equations.

Local Set Keyed Unification.

Set Default Goal Selector "!".

Implicit Types (cf : checker_flags) (Σ : global_env_ext).

#[global]
Instance red_brs_refl Σ p Γ: CRelationClasses.Reflexive (@red_brs Σ p Γ).
Proof.
  intros brs.
  eapply All2_same; unfold on_Trel; split; reflexivity.
Qed.

#[global]
Instance conv_cum_trans {cf leq} {Σ : global_env_ext} {Γ} : wf Σ RelationClasses.Transitive (@conv_cum cf leq Σ Γ).
Proof.
  intros x y z; unfold conv_cum. intros; sq.
  now etransitivity.
Qed.

Lemma closed_red_mkApps_tConst_axiom {cf} {Σ} {wfΣ : wf Σ} {Γ} {cst u} {args : list term} {cb c} :
  declared_constant Σ cst cb cst_body cb = None
  Σ ;;; Γ mkApps (tConst cst u) args c
   args' : list term,
  (c = mkApps (tConst cst u) args') × (red_terms Σ Γ args args').
Proof.
  intros decl hcb [clΓ clt r].
  eapply (PCUICConfluence.red_mkApps_tConst_axiom (Γ := exist Γ clΓ)) in decl as [args' [eq r']]; tea.
  × args'; split; auto.
    eapply into_red_terms; auto.
    inv_on_free_vars. solve_all.
  × cbn. inv_on_free_vars; solve_all.
Qed.

Conversion for PCUIC without fuel

Following PCUICSafeReduce, we derive a fuel-free implementation of conversion (and cumulativity) checking for PCUIC.

Section Conversion.

  Context {cf : checker_flags} {nor : normalizing_flags}.

  Context (X_type : abstract_env_ext_impl).

  Context (X : X_type.π1).

  Local Definition heΣ Σ (wfΣ : abstract_env_ext_rel X Σ) :
     wf_ext Σ := abstract_env_ext_wf _ wfΣ.

  Local Definition Σ (wfΣ : abstract_env_ext_rel X Σ) :
     wf Σ := abstract_env_ext_sq_wf _ _ _ wfΣ.

  Set Equations Transparent.
  Set Equations With UIP.

  Inductive state :=
  | Reduction
  | Term
  | Args
  | Fallback.

  Inductive stateR : state state Prop :=
  | stateR_Term_Reduction : stateR Term Reduction
  | stateR_Args_Term : stateR Args Term
  | stateR_Fallback_Term : stateR Fallback Term
  | stateR_Args_Fallback : stateR Args Fallback.

  Derive Signature for stateR.

  Lemma stateR_Acc :
     s, Acc stateR s.
  Proof using Type.
    assert (Acc stateR Args) as hArgs.
    { constructor. intros s h.
      dependent induction h.
      all: discriminate.
    }
    assert (Acc stateR Fallback) as hFall.
    { constructor. intros s h.
      dependent induction h.
      all: try discriminate.
      apply hArgs.
    }
    assert (Acc stateR Term) as hTerm.
    { constructor. intros s h.
      dependent induction h.
      all: try discriminate.
      - apply hArgs.
      - apply hFall.
    }
    assert (Acc stateR Reduction) as hRed.
    { constructor. intros s h.
      dependent induction h.
      all: try discriminate.
      apply hTerm.
    }
    intro s. destruct s ; eauto.
  Qed.

  Notation wtp Γ t π :=
    ( Σ (wfΣ : abstract_env_ext_rel X Σ), welltyped Σ Γ (zipc t π)) (only parsing).

  Set Primitive Projections.

  Record pack (Γ : context) := mkpack {
    st : state ;
    tm1 : term ;
    stk1 : stack ;
    tm2 : term ;
    stk2 : stack ;
    wth : wtp Γ tm2 stk2
  }.

  Arguments st {_} _.
  Arguments tm1 {_} _.
  Arguments stk1 {_} _.
  Arguments tm2 {_} _.
  Arguments stk2 {_} _.
  Arguments wth {_} _.

  Definition wterm Γ := { t : term | Σ (wfΣ : abstract_env_ext_rel X Σ), welltyped Σ Γ t }.

  Definition wcored Γ (u v : wterm Γ) :=
     Σ (wfΣ : abstract_env_ext_rel X Σ), cored' Σ Γ (` u) (` v).

  Lemma wcored_wf :
     Γ, well_founded (wcored Γ).
  Proof using Type.
    intros Γ [u hu].
    destruct (abstract_env_ext_exists X) as [[Σ wfΣ]];
    pose proof (heΣ _ wfΣ) as heΣ.
    pose proof (hu _ wfΣ) as h.
    apply normalisation_upto in h. 2: exact heΣ.
    dependent induction h.
    constructor. intros [y hy] r.
    unfold wcored in r. cbn in r.
    eapply H0. eapply r; eauto.
  Qed.

  Import PCUICAlpha.

  Definition eqt u v := u α v .

  Lemma eqt_eqterm {Σ} {wfΣ : abstract_env_ext_rel X Σ} {u v} :
    u α v eq_term Σ Σ u v.
  Proof using Type.
    intros eq.
    eapply upto_names_eq_term_refl; tc.
    exact eq.
  Qed.

  Local Instance eqt_refl : RelationClasses.Reflexive eqt.
  Proof using Type. red. intros x; constructor. reflexivity. Qed.

  Lemma eq_term_valid_pos :
     {u v p},
      validpos u p
      eqt u v
      validpos v p.
  Proof using X.
    destruct (abstract_env_ext_exists X) as [[Σ wfΣ]].
    intros u v p vp e.
    destruct e as [e'].
    eapply eq_term_valid_pos. all: eauto. now eapply eqt_eqterm.
    Unshelve. all:eauto.
  Qed.

  Definition weqt {Γ} (u v : wterm Γ) :=
    eqt (` u) (` v).

  Equations R_aux (Γ : context) :
    ( t : term, pos t × ( w : wterm Γ, pos (` w) × state))
    ( t : term, pos t × ( w : wterm Γ, pos (` w) × state)) Prop :=
    R_aux Γ :=
      t eqt \ fun t t' Σ, abstract_env_ext_rel X Σ cored' Σ Γ t t' by _
      @posR t
      w weqt \ wcored Γ by _
      @posR (` w)
      stateR.
  Next Obligation.
    split. 2: intuition eauto.
     (` p).
    destruct p as [p hp].
    eapply eq_term_valid_pos. all: eauto.
  Defined.
  Next Obligation.
    split. 2: assumption.
     (` p).
    destruct x as [u hu], x' as [v hv].
    destruct p as [p hp].
    simpl in ×.
    eapply eq_term_valid_pos. all: eauto.
  Defined.

  Derive Signature for Subterm.lexprod.

  Lemma R_aux_Acc :
     Γ t p w q s,
      ( Σ, abstract_env_ext_rel X Σ welltyped Σ Γ t)
      Acc (R_aux Γ) (t ; (p, (w ; (q, s)))).
  Proof using Type.
    intros Γ t p w q s ht.
    destruct (abstract_env_ext_exists X) as [[Σ wfΣ]].
    rewrite R_aux_equation_1.
    unshelve eapply dlexmod_Acc.
    - intros x y [e]; eauto. constructor. now symmetry.
    - intros x y z [e1] [e2]; eauto. constructor. now etransitivity; tea.
    - intro u. eapply Subterm.wf_lexprod.
      + intro. eapply posR_Acc.
      + intros [w' q'].
        unshelve eapply dlexmod_Acc.
        × intros x y [e]; eauto. constructor. now symmetry.
        × intros x y z [e1] [e2]; eauto. constructor.
          now etransitivity; tea.
        × intros [t' h']. eapply Subterm.wf_lexprod.
          -- intro. eapply posR_Acc.
          -- intro. eapply stateR_Acc.
        × intros x x' y [e] [y' [x'' [r [[e1] [e2]]]]]; eauto.
          eexists _,_. erewrite (abstract_env_ext_irr _ _ wfΣ); eauto.
          intuition eauto using sq.
          constructor. etransitivity; tea.
        × intros x.
           (@eqt_refl _).
          unfold weqt, eqt.
          intros [[q'' h] ?].
          unfold R_aux_obligations_obligation_2.
          simpl. f_equal. f_equal.
          eapply uip.
        × cbn. intros x x' [[q'' h] ?] e.
          destruct e as [e'].
          unfold R_aux_obligations_obligation_2.
          simpl. f_equal. f_equal.
          eapply uip.
        × intros x y z e1 e2 [[q'' h] ?].
          unfold R_aux_obligations_obligation_2.
          simpl. f_equal. f_equal.
          eapply uip.
        × intros [t1 ht1] [t2 ht2] e [[q1 hq1] s1] [[q2 hq2] s2] h.
          destruct e as [e'].
          simpl in ×.
          dependent destruction h.
          -- left. unfold posR in ×. simpl in ×. assumption.
          -- match goal with
             | |- context [ exist q1 ?hq1 ] ⇒
               assert (ee : hq1 = hq2) by eapply uip
             end.
            rewrite ee. right. clear ee. assumption.
        × eapply wcored_wf.
    - intros x x' y [e] [y' [x'' [r [[e1] [e2]]]]]; eauto.
      intros. erewrite (abstract_env_ext_irr _ _ wfΣ); eauto.
      eexists _,_. intuition eauto using sq.
      constructor. etransitivity; eauto.
    - intros x. (@eqt_refl _). intros [[q' h] [? [? ?]]].
      unfold R_aux_obligations_obligation_1.
      simpl. f_equal. f_equal.
      eapply uip.
    - intros x x' [[q' h] [? [? ?]]] e.
      destruct e as [e']; eauto.
      unfold R_aux_obligations_obligation_1.
      simpl. f_equal. f_equal.
      eapply uip.
    - intros x y z e1 e2 [[q' h] [? [? ?]]].
      unfold R_aux_obligations_obligation_1.
      simpl. f_equal. f_equal.
      eapply uip.
    - intros x x' e
             [[p1 hp1] [[u hu] [[q1 hq1] s1]]]
[[p2 hp2] [[v hv] [[q2 hq2] s2]]] hl.
      destruct e as [e']; eauto.
      simpl in ×.
      dependent destruction hl.
      + left. unfold posR in ×.
        simpl in ×.
        assumption.
      + match goal with
        | |- context [ exist p1 ?hp1 ] ⇒
          assert (ee : hp1 = hp2) by eapply uip
        end.
        rewrite ee. right. clear ee.
        dependent destruction H.
        × left. assumption.
        × unshelve econstructor 2. 1: assumption.
          dependent destruction H.
          -- left. unfold posR in ×.
             simpl in ×. assumption.
          -- right. assumption.
    - pose proof (heΣ _ wfΣ).
      eapply Acc_equiv; try eapply normalisation_upto; eauto.
      split; eauto; intros.
      erewrite (abstract_env_ext_irr _ _ wfΣ); eauto.
    Unshelve. all: eauto.
  Qed.

  Notation pzt u := (zipc (tm1 u) (stk1 u)) (only parsing).
  Notation pps1 u := (stack_pos (tm1 u) (stk1 u)) (only parsing).
  Notation pwt u := (exist (P := fun t Σ, abstract_env_ext_rel X Σ welltyped Σ _ t)
                                 _ (fun Σ wfΣwth u Σ wfΣ)) (only parsing).
  Notation pps2 u := (stack_pos (tm2 u) (stk2 u)) (only parsing).

  Notation obpack u:=
    (pzt u ; (pps1 u, (pwt u; (pps2 u, st u)))) (only parsing).

  Definition R Γ (u v : pack Γ) :=
    R_aux Γ (obpack u) (obpack v).

  Lemma R_Acc :
     Γ u,
      ( Σ (wfΣ : abstract_env_ext_rel X Σ), welltyped Σ Γ (zipc (tm1 u) (stk1 u)))
      Acc (R Γ) u.
  Proof using Type.
    intros Γ u h.
    eapply Acc_fun with (f := fun xobpack x).
    apply R_aux_Acc. assumption.
  Qed.

  Notation eq_term Σ t u := (eq_term Σ Σ t u).

  Lemma R_aux_irrelevance Γ x y z :
    ((x.π1; x.π2.1), (existT (fun xpos x × state) (` x.π2.2.π1) x.π2.2.π2)) =
    ((y.π1; y.π2.1), (existT (fun xpos x × state) (` y.π2.2.π1) y.π2.2.π2))
    R_aux Γ z x R_aux Γ z y.
  Proof using Type.
    destruct x as [t [pt [w [pw s]]]], y as [t' [pt' [w' [pw' s']]]].
    destruct z as [tz [ptz [wz [pwz sz]]]].
    cbn. intros [=]. subst. noconf H1. destruct w as [w wt], w' as [w' wt'].
    cbn in ×. subst w'. noconf H3.
    unfold R_aux.
    intros hr. depelim hr.
    - now constructor.
    - cbn in H.
      eapply right_dlexmod with e. cbn.
      depelim H.
      × constructor. exact H.
      × constructor 2.
        depelim H.
        + now constructor.
        + eapply right_dlexmod with e0. cbn in H.
          depelim H.
          { constructor 1. cbn. exact H. }
          { constructor 2. exact H. }
  Qed.

  Lemma R_irrelevance Γ x y z :
    (x.(st), x.(tm1), x.(stk1), x.(tm2), x.(stk2)) =
    (y.(st), y.(tm1), y.(stk1), y.(tm2), y.(stk2))
    R Γ z x R Γ z y.
  Proof using Type.
    destruct x, y; cbn.
    intros [=]; subst.
    unfold R. eapply R_aux_irrelevance; cbn.
    reflexivity.
  Qed.

  Lemma R_cored :
     Γ p1 p2,
      ( Σ (wfΣ : abstract_env_ext_rel X Σ), cored Σ Γ (pzt p1) (pzt p2))
      R Γ p1 p2.
  Proof using Type.
    intros Γ p1 p2 h.
    left. intros. eapply cored_cored'. eapply h; eauto.
  Qed.

  Lemma R_aux_positionR :
     Γ t1 t2 (p1 : pos t1) (p2 : pos t2) s1 s2,
      eqt t1 t2
      positionR (` p1) (` p2)
      R_aux Γ (t1 ; (p1, s1)) (t2 ; (p2, s2)).
  Proof using Type.
    intros Γ t1 t2 p1 p2 [? [? ?]] s2 e h.
    unshelve eright.
    - eauto.
    - left. unfold posR. simpl. assumption.
  Qed.

  Lemma R_positionR :
     Γ p1 p2,
      (eqt (pzt p1) (pzt p2))
      positionR (` (pps1 p1)) (` (pps1 p2))
      R Γ p1 p2.
  Proof using Type.
    intros Γ [s1 t1 π1 ρ1 t1' h1] [s2 t2 π2 ρ2 t2' h2] e h. simpl in ×.
    eapply R_aux_positionR ; simpl.
    - assumption.
    - assumption.
  Qed.

  Lemma R_aux_cored2 :
     Γ t1 t2 (p1 : pos t1) (p2 : pos t2) w1 w2 q1 q2 s1 s2,
      (eqt t1 t2)
      ` p1 = ` p2
      ( Σ (wfΣ : abstract_env_ext_rel X Σ), cored' Σ Γ (` w1) (` w2))
      R_aux Γ (t1 ; (p1, (w1 ; (q1, s1)))) (t2 ; (p2, (w2 ; (q2, s2)))).
  Proof using Type.
    intros Γ t1 t2 [p1 hp1] [p2 hp2] [t1' h1'] [t2' h2'] q1 q2 s1 s2 e1 e2 h.
    cbn in e2. cbn in h. subst.
    unshelve eright.
    - auto.
    - unfold R_aux_obligations_obligation_1. simpl.
      match goal with
      | |- context [ exist p2 ?hp1 ] ⇒
        assert (e : hp1 = hp2) by eapply uip
      end.
      rewrite e.
      right.
      left. assumption.
  Qed.

  Lemma R_cored2 :
     Γ p1 p2,
      (eqt (pzt p1) (pzt p2))
      ` (pps1 p1) = ` (pps1 p2)
      ( Σ (wfΣ : abstract_env_ext_rel X Σ),
          cored Σ Γ (` (pwt p1)) (` (pwt p2)))
      R Γ p1 p2.
  Proof using Type.
    intros Γ [s1 t1 π1 ρ1 t1' h1] [s2 t2 π2 ρ2 t2' h2] e1 e2 h. simpl in ×.
    eapply R_aux_cored2. all: simpl. all: auto.
    destruct s1, s2.
    all: intros; eapply cored_cored'.
    all: eauto.
  Qed.

  Lemma R_aux_positionR2 :
     Γ t1 t2 (p1 : pos t1) (p2 : pos t2) w1 w2 q1 q2 s1 s2,
      (eqt t1 t2)
      ` p1 = ` p2
      (eqt (` w1) (` w2))
      positionR (` q1) (` q2)
      R_aux Γ (t1 ; (p1, (w1 ; (q1, s1)))) (t2 ; (p2, (w2 ; (q2, s2)))).
  Proof using Type.
    intros Γ t1 t2 [p1 hp1] [p2 hp2] [t1' h1'] [t2' h2'] q1 q2 s1 s2 e1 e2 e3 h.
    cbn in e2. cbn in e3. subst.
    unshelve eright.
    - auto.
    - unfold R_aux_obligations_obligation_1. simpl.
      match goal with
      | |- context [ exist p2 ?hp1 ] ⇒
        assert (e : hp1 = hp2) by eapply uip
      end.
      rewrite e.
      right.
      unshelve eright.
      + auto.
      + left. unfold posR. simpl. assumption.
  Qed.

  Lemma R_positionR2 :
     Γ p1 p2,
      (eqt (pzt p1) (pzt p2))
      ` (pps1 p1) = ` (pps1 p2)
      (eqt (` (pwt p1)) (` (pwt p2)))
      positionR (` (pps2 p1)) (` (pps2 p2))
      R Γ p1 p2.
  Proof using Type.
    intros Γ [s1 t1 π1 ρ1 t1' h1] [s2 t2 π2 ρ2 t2' h2] e1 e2 e3 h.
    simpl in ×.
    eapply R_aux_positionR2. all: simpl. all: auto.
  Qed.

  Lemma R_aux_stateR :
     Γ t1 t2 (p1 : pos t1) (p2 : pos t2) w1 w2 q1 q2 s1 s2 ,
      (eqt t1 t2)
      ` p1 = ` p2
      (eqt (` w1) (` w2))
      ` q1 = ` q2
      stateR s1 s2
      R_aux Γ (t1 ; (p1, (w1 ; (q1, s1)))) (t2 ; (p2, (w2 ; (q2, s2)))).
  Proof using Type.
    intros Γ t1 t2 [p1 hp1] [p2 hp2] [t1' h1'] [t2' h2'] [q1 hq1] [q2 hq2] s1 s2
           e1 e2 e3 e4 h.
    cbn in e2. cbn in e3. cbn in e4. subst.
    unshelve eright.
    - auto.
    - unfold R_aux_obligations_obligation_1. simpl.
      match goal with
      | |- context [ exist p2 ?hp1 ] ⇒
        assert (e : hp1 = hp2) by eapply uip
      end.
      rewrite e.
      right.
      unshelve eright.
      + auto.
      + unfold R_aux_obligations_obligation_2. simpl.
        match goal with
        | |- context [ exist q2 ?hq1 ] ⇒
          assert (e' : hq1 = hq2) by eapply uip
        end.
        rewrite e'.
        right. assumption.
  Qed.

  Lemma R_stateR :
     Γ p1 p2,
      (eqt (pzt p1) (pzt p2))
      ` (pps1 p1) = ` (pps1 p2)
      (eqt (` (pwt p1)) (` (pwt p2)))
      ` (pps2 p1) = ` (pps2 p2)
      stateR (st p1) (st p2)
      R Γ p1 p2.
  Proof using Type.
    intros Γ [s1 t1 π1 ρ1 t1' h1] [s2 t2 π2 ρ2 t2' h2] e1 e2 e3 e4 h.
    simpl in ×.
    eapply R_aux_stateR. all: simpl. all: auto.
  Qed.

  Notation eqb_ctx := (eqb_ctx_gen (abstract_env_eq X) (abstract_env_compare_global_instance X)).
  Notation eqb_term := (eqb_term_upto_univ (abstract_env_eq X) (abstract_env_eq X) (abstract_env_compare_global_instance X)).
  Notation leqb_term := (eqb_term_upto_univ (abstract_env_eq X) (abstract_env_leq X) (abstract_env_compare_global_instance X)).

  Definition eqb_term_stack t1 π1 t2 π2 :=
    eqb_ctx (stack_context π1) (stack_context π2) &&
    eqb_term (zipp t1 π1) (zipp t2 π2).

  Lemma iff_reflect (P : Prop) (b : bool) :
    P b reflect P b.
  Proof using Type.
    intro H. apply ssrbool.introP.
    - intuition.
    - destruct b; intuition.
  Qed.

  Definition wf_universe_iff Σ u :
    wf_universeb Σ u wf_universe Σ u.
  Proof using Type.
    symmetry; apply reflect_iff. eapply wf_universe_reflect.
  Qed.

  Definition wf_universe_instance_iff Σ u :
    wf_universeb_instance Σ u wf_universe_instance Σ u.
  Proof using Type.
    symmetry; apply reflect_iff. eapply wf_universe_instanceP.
  Qed.

  Notation conv_stack_ctx Γ π1 π2 :=
    ( Σ, abstract_env_ext_rel X Σ (Σ Γ ,,, stack_context π1 = Γ ,,, stack_context π2) ).

  Notation conv_term leq Γ t π t' π' :=
    ( Σ, abstract_env_ext_rel X Σ conv_cum leq Σ (Γ ,,, stack_context π) (zipp t π) (zipp t' π'))
      (only parsing).

  Notation alt_conv_term Γ t π t' π' :=
    ( Σ, abstract_env_ext_rel X Σ Σ ;;; Γ ,,, stack_context π zipp t π = zipp t' π' )
      (only parsing).

  Inductive ConversionResult (P : Prop) :=
  | Success (h : P)
  | Error (e : ConversionError) (h : ¬P).

  Arguments Success {_} _.
  Arguments Error {_} _.

  Definition isred_full Γ t π :=
    isApp t = false
     Σ, abstract_env_ext_rel X Σ whnf RedFlags.nodelta Σ (Γ,,, stack_context π) (zipp t π).

  Lemma isred_full_nobeta Γ t π :
    isred_full Γ t π
    isLambda t
    isStackApp π = false.
  Proof using Type.
    intros (?&isr) islam.
    destruct t; cbn in *; try easy.
    unfold zipp in isr.
    destruct π as [|[]]; cbn in *; try easy.
    destruct (decompose_stack π) in isr.
    destruct (abstract_env_ext_exists X) as [[Σ wfΣ]].
    destruct (isr _ wfΣ) as [isr'].
    depelim isr'; rewrite mkApps_tApp in *; try solve [solve_discr].
    apply whne_mkApps_inv in w; [|easy].
    destruct w as [|(?&?&?&?&?&?&?&?)]; [|discriminate].
    depelim w; solve_discr; discriminate.
   Qed.

  Lemma eta_pair {A B} (p q : A × B) :
    p = q
    (p.1, p.2) = (q.1, q.2).
  Proof using Type. now destruct p, q. Qed.

  Ltac is_var t :=
    match goal with
    | v : _ |- _
      match t with
      | vidtac
      end
    end.

  Lemma zipp_stack_cat_decompose_stack t π π' :
    zipp t (π ++ (decompose_stack π').2) = zipp t π.
  Proof using Type.
    rewrite zipp_stack_cat; auto.
    destruct decompose_stack eqn:decomp.
    now apply decompose_stack_noStackApp in decomp.
  Qed.

  Lemma zipc_decompose_stack_empty t π :
    (decompose_stack π).2 = []
    zipc t π = zipp t π.
  Proof using Type.
    destruct decompose_stack eqn:decomp.
    apply decompose_stack_eq in decomp as →.
    cbn; intros →.
    rewrite zipc_appstack, zipp_as_mkApps, decompose_stack_appstack.
    cbn.
    now rewrite app_nil_r.
  Qed.

  Ltac reduce_stack_facts Σ wfΣ :=
    repeat
      match goal with
      | [H: (?a, ?b) = reduce_stack ?f _ ?X ?Γ ?t ?π ?h |- _] ⇒
        let rid := fresh "r" in
        let decompid := fresh "d" in
        let whid := fresh "w" in
        let isr := fresh "isr" in
        pose proof (reduce_stack_sound f _ X Σ wfΣ Γ t π h) as [rid];
        pose proof (reduce_stack_decompose f _ X Γ t π h) as decompid;
        pose proof (reduce_stack_whnf f _ X Γ t π h Σ wfΣ) as whid;
        pose proof (reduce_stack_isred f _ X Γ t π h) as isr;
        rewrite <- H in rid, decompid, whid, isr; cbn in rid, decompid, whid, isr;
        clear H
      end.

  Lemma zipc_unfold_decompose_stack t π :
    zipc t π = zipc (mkApps t (decompose_stack π).1) (decompose_stack π).2.
  Proof using Type.
    rewrite <- zipc_appstack.
    destruct (decompose_stack π) eqn:decomp.
    now apply decompose_stack_eq in decomp as →.
  Qed.

  Ltac simpl_stacks :=
    (repeat
       match goal with
       | [H: (?a, ?b) = decompose_stack ?π |- _] ⇒
         is_var a;
         is_var b;
         apply eta_pair in H; cbn in H; noconf H
       end);
    (repeat
       match goal with
       | [H: context[decompose_stack (appstack ?l ?ρ)] |- _] ⇒
         (rewrite (decompose_stack_appstack l ρ) in H; cbn in H) || fail 2
       | [H: context[stack_context (?π ++ ?π')] |- _] ⇒
         (rewrite (stack_context_stack_cat π' π) in H; cbn in H) || fail 2
       | [H: (decompose_stack).2 = [], H': context[stack_context ?π] |- _] ⇒
         (rewrite <- (stack_context_decompose π), H in H'; cbn in H') || fail 2
       | [H: (decompose_stack).2 = [], H': context[zipc ?t ?π] |- _] ⇒
         (rewrite (zipc_decompose_stack_empty t π H) in H'; cbn in H') || fail 2
       | [H: context[stack_context (decompose_stack).2] |- _] ⇒
         (rewrite (stack_context_decompose π) in H; cbn in H) || fail 2
       | [H: context[zipp ?t (?π ++ (decompose_stack ?π').2)] |- _] ⇒
         (rewrite (zipp_stack_cat_decompose_stack t π π') in H; cbn in H) || fail 2
       | [H: context[zipc ?t (appstack ?args ?π)] |- _] ⇒
         (rewrite (@zipc_appstack t args π) in H; cbn in H) || fail 2
       | [H: context[zipc ?t (?π ++ ?π')] |- _] ⇒
         (rewrite (zipc_stack_cat t π π') in H; cbn in H) || fail 2
       | [H: context[zip (mkApps ?t (decompose_stack).1, decompose_stack).2] |- _] ⇒
         unfold zip in H
       | [H: context[zipc (mkApps ?t (decompose_stack).1) (decompose_stack).2] |- _] ⇒
         (rewrite <- (zipc_unfold_decompose_stack t π) in H; cbn in H) || fail 2
       | [H: isStackApp= false, H': context[zipp ?t ?π] |- _] ⇒
         (rewrite (zipp_noStackApp t π H) in H'; cbn in H') || fail 2
       | [H: (decompose_stack).2 = (decompose_stack ?π').2, H': context[stack_context ?π] |- _] ⇒
         (rewrite <- (stack_context_decompose π), H, (stack_context_decompose π') in H'; cbn in H')
         || fail 2

       | [|- context[decompose_stack (appstack ?l ?ρ)]] ⇒
         (rewrite (decompose_stack_appstack l ρ); cbn) || fail 2
       | [|- context[stack_context (?π ++ ?π')]] ⇒
         (rewrite (stack_context_stack_cat π' π); cbn) || fail 2
       | [H: (decompose_stack).2 = [] |- context[stack_context ?π]] ⇒
         (rewrite <- (stack_context_decompose π), H; cbn) || fail 2
       | [H: (decompose_stack).2 = [] |- context[zipc ?t ?π]] ⇒
         (rewrite (zipc_decompose_stack_empty t π H); cbn) || fail 2
       | [|- context[stack_context (decompose_stack).2]] ⇒
         (rewrite (stack_context_decompose π); cbn) || fail 2
       | [|- context[zipp ?t (?π ++ (decompose_stack ?π').2)]] ⇒
         (rewrite (zipp_stack_cat_decompose_stack t π π'); cbn) || fail 2
       | [|- context[zipc ?t (appstack ?args ?π)]] ⇒
         (rewrite (@zipc_appstack t args π); cbn) || fail 2
       | [|- context[zipc ?t (?π ++ ?π')]] ⇒
         (rewrite (zipc_stack_cat t π π'); cbn) || fail 2
       | [|- context[zip (mkApps ?t (decompose_stack).1, decompose_stack).2]] ⇒
         unfold zip
       | [|- context[zipc (mkApps ?t (decompose_stack).1) (decompose_stack).2]] ⇒
         (rewrite <- (zipc_unfold_decompose_stack t π); cbn) || fail 2
       | [H: isStackApp= false |- context[zipp ?t ?π]] ⇒
         (rewrite (zipp_noStackApp t π H); cbn) || fail 2
       | [H: (decompose_stack).2 = (decompose_stack ?π').2 |- context[stack_context ?π]] ⇒
         (rewrite <- (stack_context_decompose π), H, (stack_context_decompose π'); cbn) || fail 2
       end);
    repeat
      match goal with
      | [H: context[zipp ?t ?π] |- _] ⇒ rewrite (zipp_as_mkApps t π) in H
      | [|- context[zipp ?t ?π]] ⇒ rewrite (zipp_as_mkApps t π)
      end.

  Ltac simpl_reduce_stack Σ wfΣ := reduce_stack_facts Σ wfΣ ; simpl_stacks.

  Equations prog_discr (t1 t2 : term) : Prop :=
    prog_discr (tApp _ _) (tApp _ _) := False ;
    prog_discr (tConst _ _) (tConst _ _) := False ;
    prog_discr (tLambda _ _ _) (tLambda _ _ _) := False ;
    prog_discr (tProd _ _ _) (tProd _ _ _) := False ;
    prog_discr (tCase _ _ _ _) (tCase _ _ _ _) := False ;
    prog_discr (tProj _ _) (tProj _ _) := False ;
    prog_discr (tFix _ _) (tFix _ _) := False ;
    prog_discr (tCoFix _ _) (tCoFix _ _) := False ;
    prog_discr _ _ := True.

  Definition Ret s Γ t π t' π' :=
     (leq : conv_pb),
      conv_stack_ctx Γ π π'
      (match s with Fallback | Termisred_full Γ t π | _True end)
      (match s with Fallback | Termisred_full Γ t' π' | _True end)
      (match s with | Fallbackprog_discr t t' | _True end)
      match s with
      | Reduction
      | Term
      | FallbackConversionResult (conv_term leq Γ t π t' π')
      | ArgsConversionResult ( Σ, abstract_env_ext_rel X Σ ws_cumul_pb_terms Σ (Γ,,, stack_context π)
                                   (decompose_stack π).1
                                   (decompose_stack π').1)
      end.

  Definition Aux s Γ t1 π1 t2 π2 h2 :=
      s' t1' π1' t2' π2'
       (h1' : wtp Γ t1' π1')
       (h2' : wtp Γ t2' π2'),
       conv_stack_ctx Γ π1 π2
       R Γ
         (mkpack Γ s' t1' π1' t2' π2' h2')
         (mkpack Γ s t1 π1 t2 π2 h2)
       Ret s' Γ t1' π1' t2' π2'.

  Notation expand aux := (fun a b c d e f g h iaux _ _ _ _ _ _ _ _ _) (only parsing).

  Local Notation yes := (Success _) (only parsing).
  Local Notation no := (fun eError e _) (only parsing).

  Local Notation repack e :=
    (match e with Success hSuccess _ | Error er hError er _ end)
    (only parsing).

  Notation isconv_red_raw leq t1 π1 t2 π2 aux :=
    (aux Reduction t1 π1 t2 π2 _ _ _ _ leq _ I I I) (only parsing).
  Notation isconv_prog_raw leq t1 π1 t2 π2 aux :=
    (aux Term t1 π1 t2 π2 _ _ _ _ leq _ _ _ I) (only parsing).
  Notation isconv_args_raw leq t1 π1 t2 π2 aux :=
    (aux Args t1 π1 t2 π2 _ _ _ _ leq _ I I I) (only parsing).
  Notation isconv_fallback_raw leq t1 π1 t2 π2 aux :=
    (aux Fallback t1 π1 t2 π2 _ _ _ _ leq _ _ _ _) (only parsing).

  Notation isconv_red leq t1 π1 t2 π2 aux :=
    (repack (isconv_red_raw leq t1 π1 t2 π2 aux)) (only parsing).
  Notation isconv_prog leq t1 π1 t2 π2 aux :=
    (repack (isconv_prog_raw leq t1 π1 t2 π2 aux)) (only parsing).
  Notation isconv_args leq t1 π1 t2 π2 aux :=
    (repack (isconv_args_raw leq t1 π1 t2 π2 aux)) (only parsing).
  Notation isconv_fallback leq t1 π1 t2 π2 aux :=
    (repack (isconv_fallback_raw leq t1 π1 t2 π2 aux)) (only parsing).

  Equations(noeqns) _isconv_red (Γ : context) (leq : conv_pb)
            (t1 : term) (π1 : stack) (h1 : wtp Γ t1 π1)
            (t2 : term) (π2 : stack) (h2 : wtp Γ t2 π2)
            (hx : conv_stack_ctx Γ π1 π2)
            (aux : Aux Reduction Γ t1 π1 t2 π2 h2)
    : ConversionResult (conv_term leq Γ t1 π1 t2 π2) :=

    _isconv_red Γ leq t1 π1 h1 t2 π2 h2 hx aux
    with inspect (decompose_stack π1) := {
    | @exist (args1, ρ1) e1 with inspect (decompose_stack π2) := {
      | @exist (args2, ρ2) e2
        with inspect (reduce_stack RedFlags.nodelta _ X
                                   (Γ ,,, stack_context π1)
                                   t1 (appstack args1 []) _) := {
        | @exist (t1',π1') eq1
          with inspect (reduce_stack RedFlags.nodelta _ X
                                     (Γ ,,, stack_context π2)
                                     t2 (appstack args2 []) _) := {
          | @exist (t2',π2') eq2isconv_prog leq t1' (π1' ++ ρ1) t2' (π2' ++ ρ2) aux
          }
        }
      }
    }.
  Next Obligation.
    symmetry in e1.
    pose proof (heΣ _ wfΣ); sq.
    eapply welltyped_zipc_stack_context ; eauto.
  Qed.
  Next Obligation.
    clear aux eq1.
    symmetry in e2.
    pose proof (heΣ _ wfΣ); sq.
    now eapply welltyped_zipc_stack_context ; eauto.
  Qed.
  Next Obligation.
    simpl_reduce_stack Σ wfΣ.
    pose proof ( _ wfΣ); sq.
    eapply red_welltyped ; try assumption ; revgoals.
    - zip fold. eapply red_context_zip. simpl_stacks. eapply r0.
    - cbn. simpl_stacks. eauto.
  Qed.
  Next Obligation.
    simpl_reduce_stack Σ wfΣ.
    pose proof ( _ wfΣ); sq.
    eapply red_welltyped ; try assumption ; revgoals.
    - zip fold. eapply red_context_zip. simpl_stacks. eapply r.
    - cbn. simpl_stacks. eauto.
  Qed.
  Next Obligation.
    match type of eq1 with
    | _ = reduce_stack ?f ?Σ ?X ?Γ ?t ?π ?h
      pose proof (reduce_stack_decompose RedFlags.nodelta _ X _ _ _ h) as d1 ;
      pose proof (reduce_stack_context f Σ X Γ t π h) as c1
    end.
    rewrite <- eq1 in d1. cbn in d1.
    rewrite <- eq1 in c1. cbn in c1.
    rewrite stack_context_appstack in c1. cbn in c1.
    pose proof (decompose_stack_eq _ _ _ (eq_sym e1)). subst.
    destruct (abstract_env_ext_exists X) as [[Σ wfΣ]].
    match type of eq1 with
    | _ = reduce_stack ?f _ ?X ?Γ ?t ?π ?hh
      pose proof (reduce_stack_Req f _ X _ wfΣ _ _ _ hh) as [ e | h ]
    end.
     - assert (ee1 := eq1). rewrite e in ee1. inversion ee1. subst.
      match type of eq2 with
      | _ = reduce_stack ?f ?Σ ?X ?Γ ?t ?π ?h
        pose proof (reduce_stack_decompose RedFlags.nodelta _ X _ _ _ h) as d2 ;
        pose proof (reduce_stack_context f Σ X Γ t π h) as c2
      end.
      rewrite <- eq2 in d2. cbn in d2.
      rewrite <- eq2 in c2. cbn in c2.
      rewrite stack_context_appstack in c2. cbn in c2.
      pose proof (decompose_stack_eq _ _ _ (eq_sym e2)). subst.
      match type of eq2 with
      | _ = reduce_stack ?f _ ?X ?Γ ?t ?π ?hh
        pose proof (reduce_stack_Req f _ X Σ wfΣ _ _ _ hh) as [ ee | h ]
      end.
      + assert (ee2 := eq2). rewrite ee in ee2. inversion ee2. subst.
        unshelve eapply R_stateR.
        × simpl. rewrite stack_cat_appstack. red. reflexivity.
        × simpl. rewrite stack_cat_appstack. reflexivity.
        × simpl. rewrite stack_cat_appstack. reflexivity.
        × simpl. rewrite stack_cat_appstack. reflexivity.
        × simpl. constructor.
      + rewrite <- eq2 in h.
        rewrite stack_context_appstack in h.
        dependent destruction h.
        × cbn in H. rewrite zipc_appstack in H. cbn in H.
          unshelve eapply R_cored2.
          -- simpl. rewrite stack_cat_appstack. reflexivity.
          -- simpl. rewrite stack_cat_appstack. reflexivity.
          -- simpl.
             rewrite zipc_appstack. rewrite zipc_stack_cat.
             repeat zip fold. intros; eapply cored_context.
             erewrite (abstract_env_ext_irr _ _ wfΣ); eauto.
        × destruct y' as [q hq].
          cbn in H0. inversion H0. subst.
          unshelve eapply R_positionR2.
          -- simpl. rewrite stack_cat_appstack. reflexivity.
          -- simpl. rewrite stack_cat_appstack. reflexivity.
          -- simpl. f_equal.
             rewrite zipc_stack_cat.
             rewrite <- H2.
             rewrite 2!zipc_appstack. cbn. reflexivity.
          -- simpl.
             unfold posR in H. cbn in H.
             rewrite stack_position_appstack in H. cbn in H.
             rewrite stack_position_stack_cat.
             rewrite stack_position_appstack.
             eapply positionR_poscat.
             assumption.
    - rewrite <- eq1 in h.
      rewrite stack_context_appstack in h.
      dependent destruction h.
      + cbn in H. rewrite zipc_appstack in H. cbn in H.
        eapply R_cored. simpl.
        rewrite zipc_appstack. rewrite zipc_stack_cat.
        repeat zip fold. intros; eapply cored_context.
        erewrite (abstract_env_ext_irr _ _ wfΣ); eauto.
      + destruct y' as [q hq].
        cbn in H0. inversion H0.         subst.
        unshelve eapply R_positionR ; simpl.
        × f_equal.
          rewrite zipc_stack_cat.
          rewrite <- H2.
          rewrite 2!zipc_appstack. cbn. reflexivity.
        × unfold posR in H. cbn in H.
          rewrite stack_position_appstack in H. cbn in H.
          rewrite stack_position_stack_cat.
          rewrite stack_position_appstack.
          eapply positionR_poscat.
          assumption.
    Unshelve. all: eauto.
  Qed.
  Next Obligation.
    rename H into wfΣ.
    simpl_reduce_stack Σ wfΣ.
    eauto.
  Qed.
  Next Obligation.
    destruct (abstract_env_ext_exists X) as [[Σ wfΣ]];
    simpl_reduce_stack Σ wfΣ.
    specialize (isr0 eq_refl) as (?&?).
    split; [easy|].
    simpl_stacks.
    intros. erewrite (abstract_env_ext_irr _ _ wfΣ); eauto.
    Unshelve. eauto.
  Qed.
  Next Obligation.
    destruct (abstract_env_ext_exists X) as [[Σ wfΣ]];
    simpl_reduce_stack Σ wfΣ.
    specialize (isr eq_refl) as (?&?).
    split; [easy|].
    simpl_stacks.
    intros. erewrite (abstract_env_ext_irr _ _ wfΣ); eauto.
    Unshelve. eauto.
  Qed.
  Next Obligation.
    rename H into wfΣ.
    simpl_reduce_stack Σ wfΣ.
    destruct ( _ wfΣ), (hx _ wfΣ).
    applyconv_cum_red_conv_iff; eauto.
    eapply h; eauto.
  Qed.
  Next Obligation.
    apply h; clear h. intros Σ wfΣ.
    simpl_reduce_stack Σ wfΣ.
    destruct ( _ wfΣ), (hx _ wfΣ).
    apply <- conv_cum_red_conv_iff; eauto.
    eapply H; eauto.
  Qed.

  Opaque reduce_stack.
  Equations unfold_one_fix (Γ : context) (mfix : mfixpoint term)
            (idx : nat) (π : stack) (h : wtp Γ (tFix mfix idx) π)
    : option (term × stack) :=

    unfold_one_fix Γ mfix idx π h with inspect (unfold_fix mfix idx) := {
    | @exist (Some (arg, fn)) eq1 with inspect (decompose_stack_at π arg) := {
      | @exist (Some (l, c, θ)) eq2 with inspect (reduce_stack RedFlags.default _ X
                                                               (Γ ,,, stack_context θ) c [] _) := {
        | @exist (cred, ρ) eq3 with construct_viewc cred := {
          | view_construct ind n ui := Some (fn, appstack l (App_l (zipc (tConstruct ind n ui) ρ) :: θ)) ;
          | view_other cred h' := None
          }
        } ;
      | _ := None
      } ;
    | _ := None
    }.
  Next Obligation.
    destruct ( _ wfΣ).
    cbn. symmetry in eq2.
    pose proof (decompose_stack_at_eq _ _ _ _ _ eq2). subst.
    rewrite zipc_appstack in h. cbn in h.
    zip fold in h. specialize (h _ wfΣ). apply welltyped_context in h ; auto. simpl in h.
    destruct h as [T h].
    apply inversion_App in h as hh ; auto.
    destruct hh as [na [A' [B' [? [? ?]]]]].
    eexists. eassumption.
  Qed.
  Transparent reduce_stack.

  Derive NoConfusion NoConfusionHom for option.

  Lemma unfold_one_fix_red_zipp :
     Γ mfix idx π h fn ξ,
      Some (fn, ξ) = unfold_one_fix Γ mfix idx π h
       Σ (wfΣ : abstract_env_ext_rel X Σ), red (fst Σ) (Γ ,,, stack_context π) (zipp (tFix mfix idx) π) (zipp fn ξ) .
  Proof using Type.
    intros Γ mfix idx π h fn ξ eq Σ wfΣ.
    revert eq.
    apply_funelim (unfold_one_fix Γ mfix idx π h); intros; try discriminate.
    all: noconf eq.
    unfold zipp.
    pose proof (eq_sym eq2) as eq.
    pose proof (decompose_stack_at_eq _ _ _ _ _ eq). subst.
    rewrite 2!decompose_stack_appstack. simpl.
    case_eq (decompose_stack θ). intros l' s' e'.
    simpl.
    match type of eq3 with
    | _ = reduce_stack ?flags _ ?X ?Γ ?t ?π ?h
      pose proof (reduce_stack_sound flags _ X Σ wfΣ Γ t π h) as [r1] ;
      pose proof (reduce_stack_decompose flags _ X Γ t π h) as hd
    end.
    rewrite <- eq3 in r1. cbn in r1.
    rewrite <- eq3 in hd. cbn in hd.
    constructor.
    rewrite stack_context_appstack. simpl.
    rewrite 2!mkApps_app. cbn. eapply red_mkApps_f.
    pose proof (decompose_stack_eq _ _ _ e'). subst.
    rewrite stack_context_appstack in r1.
    rewrite stack_context_appstack.
    eapply trans_red.
    - eapply red_app_r. exact r1.
    - repeat lazymatch goal with
      | |- context [ tApp (mkApps ?t ?l) ?u ] ⇒
        replace (tApp (mkApps t l) u) with (mkApps t (l ++ [u]))
          by (rewrite mkApps_app ; reflexivity)
      end.
      eapply red_fix.
      + symmetry. eassumption.
      + unfold is_constructor.
        pose proof (eq_sym eq2) as eql.
        apply decompose_stack_at_length in eql. subst.
        rewrite nth_error_app_ge by auto.
        replace (#|l| - #|l|) with 0 by lia. cbn.
        case_eq (decompose_stack ρ). intros l0 s1 ee.
        rewrite ee in hd.
        pose proof (decompose_stack_eq _ _ _ ee). subst.
        cbn in hd. subst.
        rewrite zipc_appstack. cbn.
        unfold isConstruct_app. rewrite decompose_app_mkApps by auto.
        reflexivity.
  Qed.

  Lemma unfold_one_fix_red_zippx :
     Γ mfix idx π h fn ξ,
      Some (fn, ξ) = unfold_one_fix Γ mfix idx π h
       Σ (wfΣ : abstract_env_ext_rel X Σ), red (fst Σ) Γ (zippx (tFix mfix idx) π) (zippx fn ξ) .
  Proof using Type.
    intros Γ mfix idx π h fn ξ eq Σ wfΣ.
    revert eq.
    apply_funelim (unfold_one_fix Γ mfix idx π h); intros; noconf eq.
    unfold zippx.
    pose proof (eq_sym eq2) as eq.
    pose proof (decompose_stack_at_eq _ _ _ _ _ eq). subst.
    rewrite 2!decompose_stack_appstack. simpl.
    case_eq (decompose_stack θ). intros l' s' e'.
    simpl.
    match type of eq3 with
    | _ = reduce_stack ?flags _ ?X ?Γ ?t ?π ?h
      pose proof (reduce_stack_sound flags _ X Σ wfΣ Γ t π h) as [r1] ;
      pose proof (reduce_stack_decompose flags _ X Γ t π h) as hd
    end.
    rewrite <- eq3 in r1. cbn in r1.
    rewrite <- eq3 in hd. cbn in hd.
    constructor. eapply red_it_mkLambda_or_LetIn.
    rewrite 2!mkApps_app. cbn. eapply red_mkApps_f.
    pose proof (decompose_stack_eq _ _ _ e'). subst.
    rewrite stack_context_appstack in r1.
    eapply trans_red.
    - eapply red_app_r. exact r1.
    - repeat lazymatch goal with
      | |- context [ tApp (mkApps ?t ?l) ?u ] ⇒
        replace (tApp (mkApps t l) u) with (mkApps t (l ++ [u]))
          by (rewrite mkApps_app ; reflexivity)
      end.
      eapply red_fix.
      + symmetry. eassumption.
      + unfold is_constructor.
        pose proof (eq_sym eq2) as eql.
        apply decompose_stack_at_length in eql. subst.
        rewrite nth_error_app_ge by auto.
        replace (#|l| - #|l|) with 0 by lia. cbn.
        case_eq (decompose_stack ρ). intros l0 s1 ee.
        rewrite ee in hd.
        pose proof (decompose_stack_eq _ _ _ ee). subst.
        cbn in hd. subst.
        rewrite zipc_appstack. cbn.
        unfold isConstruct_app. rewrite decompose_app_mkApps by auto.
        reflexivity.
  Qed.

  Lemma unfold_one_fix_red :
     Γ mfix idx π h fn ξ,
      Some (fn, ξ) = unfold_one_fix Γ mfix idx π h
       Σ (wfΣ : abstract_env_ext_rel X Σ), red (fst Σ) Γ (zipc (tFix mfix idx) π) (zipc fn ξ) .
  Proof using Type.
    intros Γ mfix idx π h fn ξ eq Σ wfΣ.
    revert eq.
    apply_funelim (unfold_one_fix Γ mfix idx π h); intros; noconf eq.
    pose proof (eq_sym eq2) as eq.
    pose proof (decompose_stack_at_eq _ _ _ _ _ eq). subst.
    rewrite !zipc_appstack. cbn.
    match type of eq3 with
    | _ = reduce_stack ?flags _ ?X ?Γ ?t ?π ?h
      pose proof (reduce_stack_sound flags _ X Σ wfΣ Γ t π h) as [r1] ;
      pose proof (reduce_stack_decompose flags _ X Γ t π h) as hd
    end.
    clear Heq1 Heq2. cbn in r1.
    rewrite <- eq3 in r1. cbn in r1.
    rewrite <- eq3 in hd. cbn in hd.
    do 2 zip fold. constructor. eapply red_context_zip.
    eapply trans_red.
    - eapply red_app_r. exact r1.
    - repeat lazymatch goal with
      | |- context [ tApp (mkApps ?t ?l) ?u ] ⇒
        replace (tApp (mkApps t l) u) with (mkApps t (l ++ [u]))
          by (rewrite mkApps_app ; reflexivity)
      end.
      eapply red_fix.
      + symmetry. eassumption.
      + unfold is_constructor.
        pose proof (eq_sym eq2) as eql.
        apply decompose_stack_at_length in eql. subst.
        rewrite nth_error_app_ge by auto.
        replace (#|l| - #|l|) with 0 by lia. cbn.
        case_eq (decompose_stack ρ). intros l0 s1 ee.
        rewrite ee in hd.
        pose proof (decompose_stack_eq _ _ _ ee). subst.
        cbn in hd. subst.
        rewrite zipc_appstack. cbn.
        unfold isConstruct_app. rewrite decompose_app_mkApps by auto.
        reflexivity.
  Qed.

  Lemma unfold_one_fix_cored :
     Γ mfix idx π h fn ξ,
      Some (fn, ξ) = unfold_one_fix Γ mfix idx π h
       Σ (wfΣ : abstract_env_ext_rel X Σ), cored (fst Σ) Γ (zipc fn ξ) (zipc (tFix mfix idx) π).
  Proof using Type.
    intros Γ mfix idx π h fn ξ eq Σ wfΣ.
    revert eq.
    apply_funelim (unfold_one_fix Γ mfix idx π h); intros ; noconf eq.
    pose proof (eq_sym eq2) as eq.
    pose proof (decompose_stack_at_eq _ _ _ _ _ eq). subst.
    rewrite !zipc_appstack. cbn.
    match type of eq3 with
    | _ = reduce_stack ?flags _ ?X ?Γ ?t ?π ?h
      pose proof (reduce_stack_sound flags _ X Σ wfΣ Γ t π h) as [r1] ;
      pose proof (reduce_stack_decompose flags _ X Γ t π h) as hd
    end.
    rewrite <- eq3 in r1. cbn in r1.
    rewrite <- eq3 in hd. cbn in hd.
    do 2 zip fold. eapply cored_context.
    eapply cored_red_trans.
    - eapply red_app_r. exact r1.
    - repeat lazymatch goal with
      | |- context [ tApp (mkApps ?t ?l) ?u ] ⇒
        replace (tApp (mkApps t l) u) with (mkApps t (l ++ [u]))
          by (rewrite mkApps_app ; reflexivity)
      end.
      eapply red_fix.
      + symmetry. eassumption.
      + unfold is_constructor.
        pose proof (eq_sym eq2) as eql.
        apply decompose_stack_at_length in eql. subst.
        rewrite nth_error_app_ge by auto.
        replace (#|l| - #|l|) with 0 by lia. cbn.
        case_eq (decompose_stack ρ). intros l0 s1 ee.
        rewrite ee in hd.
        pose proof (decompose_stack_eq _ _ _ ee). subst.
        cbn in hd. subst.
        rewrite zipc_appstack. cbn.
        unfold isConstruct_app. rewrite decompose_app_mkApps by auto.
        reflexivity.
  Qed.

  Lemma unfold_one_fix_decompose :
     Γ mfix idx π h fn ξ,
      Some (fn, ξ) = unfold_one_fix Γ mfix idx π h
      snd (decompose_stack π) = snd (decompose_stack ξ).
  Proof using Type.
    intros Γ mfix idx π h fn ξ eq.
    revert eq.
    apply_funelim (unfold_one_fix Γ mfix idx π h); intros; noconf eq.
    pose proof (eq_sym eq2) as eq.
    pose proof (decompose_stack_at_eq _ _ _ _ _ eq). subst.
    rewrite 2!decompose_stack_appstack. cbn.
    case_eq (decompose_stack θ). intros l0 s1 H2.
    reflexivity.
  Qed.

  Lemma unfold_one_fix_None Γ mfix idx π wf :
    None = unfold_one_fix Γ mfix idx π wf
    args,
      Σ (wfΣ : abstract_env_ext_rel X Σ),
      All2 (red Σ (Γ,,, stack_context π)) (decompose_stack π).1 args ×
      whnf RedFlags.default Σ (Γ,,, stack_context π) (mkApps (tFix mfix idx) args).
  Proof using Type.
    funelim (unfold_one_fix Γ mfix idx π wf).
    all: intros [=].
    - constructor; eexists _; split; [apply All2_same; reflexivity|].
      eapply whnf_fixapp.
      now rewrite <- e.
    - constructor; eexists _; split; [apply All2_same; reflexivity|].
      eapply whnf_fixapp.
      rewrite <- eq1.
      destruct (decompose_stack π) eqn:decomp.
      apply decompose_stack_noStackApp in decomp as ?.
      apply decompose_stack_eq in decomp as →.
      clear H.
      symmetry in e.
      now apply decompose_stack_at_appstack_None in e.
    - destruct (abstract_env_ext_exists X) as [[Σ wfΣ]].
      match type of eq3 with
      | _ = reduce_stack ?a ?b ?c ?d ?e ?f ?g
        pose proof (reduce_stack_sound a b c Σ wfΣ d e f g) as [r];
        pose proof (reduce_stack_whnf a b c d e f g) as wh;
        pose proof (reduce_stack_decompose a b c d e f g) as decomp;
        pose proof (reduce_stack_isred a b c d e f g) as isr
      end.
      rewrite <- eq3 in r, wh, decomp, isr.
      specialize (isr eq_refl) as (noapp&_).
      cbn in ×.
      clear H eq3 H0.
      destruct (heΣ Σ wfΣ).
      symmetry in eq2.
      apply decompose_stack_at_length in eq2 as ?.
      apply decompose_stack_at_eq in eq2 as →.
      rewrite stack_context_appstack.
      cbn. specialize (h Σ wfΣ).
      apply welltyped_zipc_zipp in h; auto.
      rewrite <- (stack_context_decompose ρ), decomp in wh.
      change (App_l c :: θ) with (appstack [c] θ) in ×.
      rewrite !decompose_stack_appstack.
      rewrite zipp_as_mkApps, !decompose_stack_appstack in h.
      destruct h as (ty&typ).
      cbn in ×.
      rewrite stack_context_appstack in typ.
      cbn in ×.
      destruct (decompose_stack ρ) eqn:decomp'.
      apply decompose_stack_eq in decomp' as →.
      rewrite zipc_appstack in r.
      rewrite zipp_appstack in wh.
      cbn in *; subst; cbn in ×.
      destruct ( Σ wfΣ), (wh Σ wfΣ).
      constructor; (l ++ (mkApps cred l0) :: (decompose_stack θ).1).
      intros. erewrite (abstract_env_ext_irr _ _ wfΣ); eauto.
      eapply PCUICSR.subject_reduction in typ.
      2: eauto.
      2: apply red_mkApps; [reflexivity|].
      1: split.
      1,3: apply All2_app; [apply All2_same; reflexivity|].
      1,2: constructor; [|apply All2_same; reflexivity].
      1-2: eapply r.
      apply whnf_ne.
      econstructor.
      + eauto.
      + rewrite nth_error_snoc by easy.
        eauto.
      + eapply whnf_fix_arg_whne; eauto.
        now destruct cred.
      Unshelve. eauto.
  Qed.

  Inductive prog_view : term term Type :=
  | prog_view_App u1 v1 u2 v2 :
      prog_view (tApp u1 v1) (tApp u2 v2)

  | prog_view_Const c1 u1 c2 u2 :
      prog_view (tConst c1 u1) (tConst c2 u2)

  | prog_view_Lambda na1 A1 b1 na2 A2 b2 :
      prog_view (tLambda na1 A1 b1) (tLambda na2 A2 b2)

  | prog_view_Prod na1 A1 B1 na2 A2 B2 :
      prog_view (tProd na1 A1 B1) (tProd na2 A2 B2)

  | prog_view_Case ci p c brs ci' p' c' brs' :
      prog_view (tCase ci p c brs) (tCase ci' p' c' brs')

  | prog_view_Proj p c p' c' :
      prog_view (tProj p c) (tProj p' c')

  | prog_view_Fix mfix idx mfix' idx' :
      prog_view (tFix mfix idx) (tFix mfix' idx')

  | prog_view_CoFix mfix idx mfix' idx' :
      prog_view (tCoFix mfix idx) (tCoFix mfix' idx')

  | prog_view_other :
       u v, prog_discr u v prog_view u v.

  Equations prog_viewc u v : prog_view u v :=
    prog_viewc (tApp u1 v1) (tApp u2 v2) :=
      prog_view_App u1 v1 u2 v2 ;

    prog_viewc (tConst c1 u1) (tConst c2 u2) :=
      prog_view_Const c1 u1 c2 u2 ;

    prog_viewc (tLambda na1 A1 b1) (tLambda na2 A2 b2) :=
      prog_view_Lambda na1 A1 b1 na2 A2 b2 ;

    prog_viewc (tProd na1 A1 B1) (tProd na2 A2 B2) :=
      prog_view_Prod na1 A1 B1 na2 A2 B2 ;

    prog_viewc (tCase ci p c brs) (tCase ci' p' c' brs') :=
      prog_view_Case ci p c brs ci' p' c' brs' ;

    prog_viewc (tProj p c) (tProj p' c') :=
      prog_view_Proj p c p' c' ;

    prog_viewc (tFix mfix idx) (tFix mfix' idx') :=
      prog_view_Fix mfix idx mfix' idx' ;

    prog_viewc (tCoFix mfix idx) (tCoFix mfix' idx') :=
      prog_view_CoFix mfix idx mfix' idx' ;

    prog_viewc u v := prog_view_other u v I.

  Lemma welltyped_wf_local Σ Γ t :
    welltyped Σ Γ t
     wf_local Σ Γ .
  Proof using Type.
    intros []; sq.
    eapply typing_wf_local in X0; eauto.
  Qed.

  Definition eqb_universe_instance_gen eq u v :=
    forallb2 eq (map Universe.make u) (map Universe.make v).

  Definition eqb_universe_instance :=
    eqb_universe_instance_gen (abstract_env_eq X).

  Lemma eqb_universe_instance_spec :
     u v Σ (wfΣ : abstract_env_ext_rel X Σ),
      forallb (wf_universeb Σ) (map Universe.make u)
      forallb (wf_universeb Σ) (map Universe.make v)
      eqb_universe_instance u v
      R_universe_instance (eq_universe (global_ext_constraints Σ)) u v.
  Proof using Type.
    intros u v Σ wfΣ Hu Hv e.
    unfold eqb_universe_instance in e.
    eapply forallb2_Forall2 in e.
    eapply forallb_Forall in Hu.
    eapply forallb_Forall in Hv.
    eapply Forall_Forall2_and in e; try exact Hu; clear Hu.
    eapply Forall_Forall2_and' in e; try exact Hv; clear Hv.
    eapply Forall2_impl. 1: eassumption.
    intros. cbn in H. destruct H as [[Hx H] Hy].
    eapply (abstract_env_compare_universe_correct _ _ Conv); eauto; now eapply wf_universe_iff.
  Unshelve. eauto.
  Qed.

  Arguments LevelSet.mem : simpl never.

  Definition abstract_conv_pb_relb `{cf : checker_flags}
    (pb : conv_pb) :=
    match pb with
    | Convabstract_env_eq X
    | Cumulabstract_env_leq X
    end.

  Lemma compare_universeb_complete Σ (wfΣ : abstract_env_ext_rel X Σ) leq u u' :
    wf_universe Σ u
    wf_universe Σ u'
    compare_universe leq (global_ext_constraints Σ) u u'
    abstract_conv_pb_relb leq u u'.
  Proof using Type.
    intros all1 all2 conv.
    destruct (heΣ _ wfΣ).
    destruct leq; eapply (abstract_env_compare_universe_correct _ _ _); eauto.
    Unshelve. all: eauto.
Qed.

  Lemma get_level_make l :
    LevelExpr.get_level (LevelExpr.make l) = l.
  Proof using Type. now destruct l. Qed.

  Lemma compare_universeb_make_complete Σ (wfΣ : abstract_env_ext_rel X Σ) leq x y :
    wf_universe_level Σ x
    wf_universe_level Σ y
    compare_universe leq (global_ext_constraints Σ) (Universe.make x) (Universe.make y)
    abstract_conv_pb_relb leq (Universe.make x) (Universe.make y).
  Proof using Type.
    intros wfx wfy r.
    eapply compare_universeb_complete; eauto.
    - intros ? ->%LevelExprSet.singleton_spec; auto.
    - intros ? ->%LevelExprSet.singleton_spec; auto.
  Qed.

  Lemma eqb_universe_instance_complete Σ (wfΣ : abstract_env_ext_rel X Σ) u u' :
    wf_universe_instance Σ u
    wf_universe_instance Σ u'
    R_universe_instance (eq_universe (global_ext_constraints Σ)) u u'
    eqb_universe_instance u u'.
  Proof using Type.
    intros memu memu' r.
    induction u in u', memu, memu', r |- ×.
    - now destruct u'.
    - destruct u'; [easy|].
      depelim memu.
      depelim memu'.
      depelim r.
      cbn in ×.
      apply Bool.andb_true_iff.
      split.
      + eapply (compare_universeb_make_complete _ _ Conv); eauto.
      + apply IHu; eauto.
  Unshelve. all:eauto.
  Qed.

  Lemma compare_universe_variance_complete Σ (wfΣ : abstract_env_ext_rel X Σ) leq v u u' :
    wf_universe_level Σ u
    wf_universe_level Σ u'
    R_universe_variance (eq_universe Σ) (compare_universe leq Σ) v u u'
    compare_universe_variance (abstract_env_eq X) (abstract_conv_pb_relb leq) v u u'.
  Proof using Type.
    intros memu memu' r.
    destruct v; cbn in *; eauto.
    - eapply compare_universeb_make_complete; eauto.
    - eapply (compare_universeb_make_complete _ _ Conv); eauto.
    Unshelve. eauto.
  Qed.

  Lemma compare_universe_instance_variance_complete Σ (wfΣ : abstract_env_ext_rel X Σ) leq v u u' :
    wf_universe_instance Σ u
    wf_universe_instance Σ u'
    R_universe_instance_variance (eq_universe Σ) (compare_universe leq Σ) v u u'
    compare_universe_instance_variance (abstract_env_eq X) (abstract_conv_pb_relb leq) v u u'.
  Proof using Type.
    intros memu memu' r.
    induction u in v, u', memu, memu', r |- ×.
    - now destruct u'.
    - destruct u'; [easy|].
      depelim memu.
      depelim memu'.
      cbn in ×.
      destruct v; auto.
      apply Bool.andb_true_iff.
      destruct r.
      split.
      + eapply compare_universe_variance_complete; eauto.
      + now apply IHu.
  Qed.

  Lemma compare_global_instance_complete Σ (wfΣ : abstract_env_ext_rel X Σ) u v leq gr napp :
    wf_universe_instance Σ u
    wf_universe_instance Σ v
    R_global_instance Σ (eq_universe Σ) (compare_universe leq Σ) gr napp u v
    compare_global_instance Σ (abstract_env_eq X) (abstract_conv_pb_relb leq) gr napp u v.
  Proof using Type.
    intros consu consv r.
    unfold compare_global_instance, R_global_instance, R_opt_variance in ×.
    destruct global_variance.
    - eapply compare_universe_instance_variance_complete; eauto.
    - eapply eqb_universe_instance_complete; eauto.
  Qed.

  Lemma consistent_instance_ext_wf Σ udecl u :
    consistent_instance_ext Σ udecl u
    wf_universe_instance Σ u.
  Proof using Type.
    intros cons.
    unfold consistent_instance_ext, consistent_instance in ×.
    destruct udecl.
    - destruct u; cbn in *; [|congruence].
      constructor.
    - destruct cons as (mems&_&_).
      apply forallb_Forall in mems.
      eapply Forall_impl; eauto.
      cbn.
      intros ? ?%LevelSet.mem_spec; auto.
  Qed.

  Lemma welltyped_zipc_tConst_inv Σ (wfΣ : abstract_env_ext_rel X Σ) Γ c u π :
    welltyped Σ Γ (zipc (tConst c u) π)
     cst,
      declared_constant Σ c cst
      × consistent_instance_ext Σ (cst_universes cst) u.
  Proof using Type.
    intros h.
    zip fold in h.
    destruct (heΣ _ wfΣ).
    apply welltyped_context in h; auto.
    destruct h as (?&typ).
    apply inversion_Const in typ as (?&?&?&wfu&_); auto.
    now unfold declared_constant in d.
  Qed.

  Lemma red_conv_cum_l {leq Γ u v Σ}{wfΣ : abstract_env_ext_rel X Σ} :
    Σ ;;; Γ u v conv_cum leq Σ Γ u v.
  Proof using Type.
    intros r. pose proof ( _ wfΣ). sq. now apply red_ws_cumul_pb.
  Qed.

  Lemma red_conv_cum_r {leq Γ u v Σ}{wfΣ : abstract_env_ext_rel X Σ} :
    Σ ;;; Γ u v conv_cum leq Σ Γ v u.
  Proof using Type.
    intros r. pose proof ( _ wfΣ). sq. now apply red_ws_cumul_pb_inv.
  Qed.

  Lemma closed_red_zipp {Σ Γ t u π} :
    is_open_term Γ (zipp t π)
    Σ ;;; Γ t u
    Σ ;;; Γ zipp t π zipp u π.
  Proof using Type.
    intros cltπ [clΓ clt r].
    eapply into_closed_red; tea.
    now eapply red_zipp.
  Qed.

  Ltac specialize_Σ wfΣ :=
    repeat match goal with | h : _ |- _specialize (h _ wfΣ) end.

  Equations(noeqns) unfold_constants (Γ : context) (leq : conv_pb)
            (c : kername) (u : Instance.t) (π1 : stack)
            (h1 : wtp Γ (tConst c u) π1)
            (c' : kername) (u' : Instance.t) (π2 : stack)
            (h2 : wtp Γ (tConst c' u') π2)
            (ne : c c' (c = c' ¬eqb_universe_instance u u'))
            (hx : conv_stack_ctx Γ π1 π2)
            (aux : Aux Term Γ (tConst c u) π1 (tConst c' u') π2 h2)
    : ConversionResult (conv_term leq Γ (tConst c u) π1 (tConst c' u') π2) :=

    unfold_constants Γ leq c u π1 h1 c' u' π2 h2 ne hx aux
    with inspect (abstract_env_lookup X c') := {
    | @exist (Some (ConstantDecl {| cst_body := Some b |})) eq1 :=
      isconv_red leq (tConst c u) π1 (subst_instance u' b) π2 aux ;
    
    | @exist _ eq1 with inspect (abstract_env_lookup X c) := {
      | @exist (Some (ConstantDecl {| cst_body := Some b |})) eq2 :=
        isconv_red leq (subst_instance u b) π1
                        (tConst c' u') π2 aux ;
      
      | @exist _ eq2 := no (NotFoundConstants c c')
      }
    }.
  Ltac solve_unfold_constants aux eq1 eq2 Σ wfΣ :=
  try destruct (abstract_env_ext_exists X) as [[Σ wfΣ]];
  exfalso;
  Tactics.program_simplify;
  CoreTactics.equations_simpl;
  try erewrite <- abstract_env_lookup_correct in eq1; eauto ;
  try erewrite <- abstract_env_lookup_correct in eq2; eauto ;
  try clear aux; specialize_Σ wfΣ;
  solve
      [match goal with
       | [H: welltyped ?Σ ?Γ ?t |- _] ⇒
         let id := fresh in
         apply welltyped_zipc_tConst_inv in H as id; eauto;
           destruct id as (?&?&?);
           unfold declared_constant in *;
           congruence
       end].

  Next Obligation.
    try rewrite <- wf_env_lookup_correct in eq1.
    pose proof ( _ wfΣ).
    sq.
    eapply red_welltyped; try eapply h2; eauto.
    eapply red_zipc.
    eapply red_const. erewrite abstract_env_lookup_correct; eauto.
  Qed.
  Next Obligation.
    unshelve eapply R_cored2.
    all: try reflexivity.
    simpl. intros. eapply cored_zipc.
    eapply cored_const. erewrite abstract_env_lookup_correct; eassumption.
  Qed.
  Next Obligation.
    rename H into wfΣ; destruct ( _ wfΣ).
    etransitivity; try eauto.
    eapply red_conv_cum_r ; try assumption.
    specialize (hx _ wfΣ).
    eapply closed_red_zipp.
    × clear aux. eapply welltyped_zipc_zipp in h2; eauto.
      eapply welltyped_is_open_term in h2.
      sq. now rewrite (All2_fold_length hx).
    × eapply into_closed_red; fvs.
      + eapply red_const. erewrite abstract_env_lookup_correct; eauto.
      + red in h. sq. fvs.
   Unshelve. eauto.
  Qed.
  Next Obligation.
    apply h; clear h. intros Σ wfΣ.
    destruct ( _ wfΣ).
    etransitivity ; try eauto.
    specialize (hx _ wfΣ).
    eapply red_conv_cum_l ; try assumption.
    eapply closed_red_zipp.
    × clear aux; eapply welltyped_zipc_zipp in h2; eauto.
      eapply welltyped_is_open_term in h2. sq. now rewrite (All2_fold_length hx).
    × eapply into_closed_red; fvs.
      + eapply red_const. erewrite abstract_env_lookup_correct; eauto.
      + sq. fvs.
  Unshelve. eauto.
  Qed.
  Next Obligation.
    pose proof ( _ wfΣ). sq.
    eapply red_welltyped ; [eauto|exact (h1 _ wfΣ)|..].
    eapply red_zipc.
    eapply red_const. erewrite abstract_env_lookup_correct; eauto.
  Qed.
  Next Obligation.
    eapply R_cored. simpl. intros. eapply cored_zipc.
    eapply cored_const. erewrite abstract_env_lookup_correct; eauto.
  Qed.
  Next Obligation.
    rename H into wfΣ. destruct (heΣ _ wfΣ) as [].
    etransitivity ; try eauto.
    eapply red_conv_cum_l ; try assumption.
    eapply closed_red_zipp.
    { eapply welltyped_zipc_zipp in h1; auto; fvs. }
    eapply into_closed_red; fvs.
    + eapply red_const. erewrite abstract_env_lookup_correct; eauto.
    + specialize (hx _ wfΣ). clear -hx . sq. fvs.
    Unshelve. all : eauto.
  Qed.
  Next Obligation.
    apply h; clear h. intros Σ wfΣ.
    destruct ( _ wfΣ) as [].
    etransitivity ; try eauto.
    eapply red_conv_cum_r ; try assumption.
    eapply closed_red_zipp.
    { eapply welltyped_zipc_zipp in h1; auto; fvs. }
    eapply into_closed_red; fvs.
    + eapply red_const. erewrite abstract_env_lookup_correct; eauto.
    + specialize (hx _ wfΣ). sq; fvs.
    Unshelve. eauto.
  Qed.
  Next Obligation.
      destruct (abstract_env_ext_exists X) as [[Σ wfΣ]].
      specialize (H _ wfΣ).
      apply conv_cum_alt in H as [(?&?&[r1 r2 eq])]; auto.
    2: pose proof ( _ wfΣ); sq ; eauto.
    rewrite zipp_as_mkApps in r1, r2.
    erewrite <- abstract_env_lookup_correct in eq1, eq2; eauto.
    symmetry in eq1, eq2.
    generalize . intros []; eauto.
    unshelve eapply closed_red_mkApps_tConst_axiom in r1 as (?&->&?); eauto.
    eapply closed_red_mkApps_tConst_axiom in r2 as (?&->&?); eauto.
    apply eq_termp_mkApps_inv in eq as (eq&?); [|easy|easy].
    depelim eq.
    destruct ne as [|(_&ne)]; [congruence|].

    clear aux. specialize (h1 _ wfΣ). specialize (h2 _ wfΣ).
    apply welltyped_zipc_tConst_inv in h1 as (cst1&decl1&cons1); eauto.
    apply welltyped_zipc_tConst_inv in h2 as (cst2&decl2&cons2); eauto.
    eapply declared_constant_inj in decl1; eauto; subst.
    apply consistent_instance_ext_wf in cons1.
    apply consistent_instance_ext_wf in cons2.
    eapply eqb_universe_instance_complete in r; auto.
  Qed.
  Next Obligation. solve_unfold_constants aux eq1 eq2 Σ wfΣ. Qed.
  Next Obligation. solve_unfold_constants aux eq1 eq2 Σ wfΣ. Qed.
  Next Obligation. solve_unfold_constants aux eq1 eq2 Σ wfΣ. Qed.
  Next Obligation. solve_unfold_constants aux eq1 eq2 Σ wfΣ. Qed.
  Next Obligation. solve_unfold_constants aux eq1 eq2 Σ H. Qed.
  Next Obligation. solve_unfold_constants aux eq1 eq2 Σ wfΣ. Qed.
  Next Obligation. solve_unfold_constants aux eq1 eq2 Σ wfΣ. Qed.
  Next Obligation. solve_unfold_constants aux eq1 eq2 Σ wfΣ. Qed.
  Next Obligation. solve_unfold_constants aux eq1 eq2 Σ wfΣ. Qed.
  Next Obligation. solve_unfold_constants aux eq1 eq2 Σ wfΣ. Qed.
  Next Obligation. solve_unfold_constants aux eq1 eq2 Σ wfΣ. Qed.
  Next Obligation. solve_unfold_constants aux eq1 eq2 Σ H. Qed.
  Next Obligation. solve_unfold_constants aux eq1 eq2 Σ wfΣ. Qed.
  Next Obligation. solve_unfold_constants aux eq1 eq2 Σ wfΣ. Qed.
  Next Obligation. solve_unfold_constants aux eq1 eq2 Σ wfΣ. Qed.
  Next Obligation. solve_unfold_constants aux eq1 eq2 Σ wfΣ. Qed.

  Lemma welltyped_zipc_tCase_brs_length Σ (wfΣ : abstract_env_ext_rel X Σ) Γ ci motive discr brs π :
    welltyped Σ Γ (zipc (tCase ci motive discr brs) π)
     mib oib, declared_inductive Σ ci mib oib #|brs| = #|ind_ctors oib|.
  Proof using Type.
    pose proof ( _ wfΣ). sq.
    intros wf.
    zip fold in wf.
    apply welltyped_context in wf; [|auto].
    destruct wf as [ctyp typ].
    apply inversion_Case in typ as (mdecl&idecl&?&?&[]&?); auto.
     mdecl, idecl.
    split; [easy|].
    now apply All2i_length in brs_ty.
  Qed.

  Equations (noeqns) isconv_context_aux
            (Γ Γ' Δ Δ' : context)
            (cc : Σ (wfΣ : abstract_env_ext_rel X Σ), Σ Γ = Γ')
            (check :
                (leq : conv_pb) (Δh : context_hole) (t : term) (Δh' : context_hole) (t' : term),
                 Δ = fill_context_hole Δh t
                 Δ' = fill_context_hole Δh' t'
                 ( Σ (wfΣ : abstract_env_ext_rel X Σ), ws_cumul_ctx_pb_rel Conv Σ Γ (context_hole_context Δh) (context_hole_context Δh'))
                 ConversionResult ( Σ (wfΣ : abstract_env_ext_rel X Σ), conv_cum leq Σ (Γ,,, context_hole_context Δh) t t'))
            (Δpre Δ'pre Δpost Δ'post : context)
            (eq : Δ = Δpre ,,, Δpost)
            (eq' : Δ' = Δ'pre ,,, Δ'post) :
    ConversionResult ( Σ (wfΣ : abstract_env_ext_rel X Σ), ws_cumul_ctx_pb_rel Conv Σ Γ Δpre Δ'pre) by struct Δpre := {

    isconv_context_aux Γ Γ' Δ Δ' cc check [] [] Δpost Δ'post eq eq'yes;

    isconv_context_aux Γ Γ' Δ Δ' cc check
                           (mkdecl na bd ty :: Δpre)
                           (mkdecl na' bd' ty' :: Δ'pre)
                           Δpost Δ'post eq eq'
      with isconv_context_aux
             Γ Γ' Δ Δ' cc check Δpre Δ'pre
             (Δpost ++ [mkdecl na bd ty])
             (Δ'post ++ [mkdecl na' bd' ty']) _ _ := {

      | Error ce not_conv_restno ce;

      | Success conv_rest
        with inspect (eqb_binder_annot na na') := {
        
        | exist false neq_bindersno (ContextNotConvertibleAnn
                                           (Γ,,, Δpre) (mkdecl na bd ty)
                                           (Γ',,, Δ'pre) (mkdecl na' bd' ty'));

        | exist true eq_binders
          with check Conv
               (Δpre, decl_hole_type na bd, Δpost) ty
               (Δ'pre, decl_hole_type na' bd', Δ'post) ty'
               _ _ conv_rest := {

          | Error ce not_conv_typeno (ContextNotConvertibleType
                                            (Γ,,, Δpre) (mkdecl na bd ty)
                                            (Γ',,, Δ'pre) (mkdecl na' bd' ty'));

          | Success conv_type with bd, bd' := {
            
            | Some body | Some body'
                with check Conv
                     (Δpre, decl_hole_body na ty, Δpost) body
                     (Δ'pre, decl_hole_body na' ty', Δ'post) body'
                     _ _ conv_rest := {
              | Error ce not_conv_bodyno (ContextNotConvertibleBody
                                                (Γ,,, Δpre) (mkdecl na bd ty)
                                                (Γ',,, Δ'pre) (mkdecl na' bd' ty'));
              
              | Success conv_bodyyes
              };

            | None | Noneyes;

            | _ | _no (ContextNotConvertibleBody
                             (Γ,,, Δpre) (mkdecl na bd ty)
                             (Γ',,, Δ'pre) (mkdecl na' bd' ty'))
            }
          }
        }
      };

    isconv_context_aux Γ Γ' Δ Δ' cc check
                       Δpre Δ'pre Δpost Δ'post eq eq'no ContextNotConvertibleLength
    }.
  Next Obligation.
    pose proof (heΣ _ wfΣ). specialize (cc _ wfΣ). sq.
    constructor; fvs.
    - constructor.
  Qed.
  Next Obligation.
    destruct (abstract_env_ext_exists X) as [[Σ wfΣ]];
    pose proof ( _ wfΣ). specialize (H _ wfΣ). sq.
    depelim H. depelim a.
  Qed.
  Next Obligation.
  destruct (abstract_env_ext_exists X) as [[Σ wfΣ]];
  pose proof ( _ wfΣ). specialize (H _ wfΣ). sq.
  destruct H as [H]; depelim H. depelim a.
  Qed.
  Next Obligation.
    unfold app_context.
    rewrite <- app_assoc; auto.
  Qed.
  Next Obligation.
    unfold app_context.
    rewrite <- app_assoc; auto.
  Qed.
  Next Obligation.
    unfold conv_cum in conv_type, conv_body.
    pose proof ( _ wfΣ). specialize_Σ wfΣ.
    sq. constructor; fvs.
    constructor; auto.
    × now destruct conv_rest.
    × constructor; auto.
      apply eqb_annot_spec; auto.
  Qed.
  Next Obligation.
    destruct (abstract_env_ext_exists X) as [[Σ wfΣ]];
    pose proof ( _ wfΣ). specialize (H _ wfΣ). sq.
    destruct H as [H].
    contradiction not_conv_body.
    depelim H.
    depelim a. depelim a0. intros.
    erewrite (abstract_env_ext_irr _ _ wfΣ); eauto.
    constructor; auto.
    Unshelve. all: eauto.
  Qed.
  Next Obligation.
    destruct (abstract_env_ext_exists X) as [[Σ wfΣ]];
    pose proof ( _ wfΣ). specialize (H _ wfΣ). sq.
    destruct H as [H].
    depelim H.
    depelim a. depelim a0.
  Qed.
  Next Obligation.
    destruct (abstract_env_ext_exists X) as [[Σ wfΣ]];
    pose proof ( _ wfΣ). specialize (H _ wfΣ). sq.
    destruct H as [H].
    depelim H.
    depelim a. depelim a0.
  Qed.
  Next Obligation.
    red in conv_type. pose proof ( _ wfΣ). specialize_Σ wfΣ.
    sq. constructor; fvs.
    constructor; auto.
    × now destruct conv_rest.
    × constructor; auto.
      apply eqb_annot_spec; auto.
  Qed.
  Next Obligation.
    destruct (abstract_env_ext_exists X) as [[Σ wfΣ]];
    pose proof ( _ wfΣ). specialize (H _ wfΣ). sq.
    destruct H as [H].
    contradiction not_conv_type.
    depelim H. intros.
    erewrite (abstract_env_ext_irr _ _ wfΣ); eauto.
    constructor.
    depelim a; auto. depelim a0; eauto.
    Unshelve. all: eauto.
  Qed.
  Next Obligation.
    destruct (abstract_env_ext_exists X) as [[Σ wfΣ]];
    pose proof ( _ wfΣ). specialize (H _ wfΣ). sq.
    destruct H as [H].
    depelim H.
    depelim a. depelim a0.
    - apply eqb_annot_spec in eqna; congruence.
    - apply eqb_annot_spec in eqna; congruence.
  Qed.
  Next Obligation.
    destruct (abstract_env_ext_exists X) as [[Σ wfΣ]];
    pose proof ( _ wfΣ). specialize (H _ wfΣ). sq.
    destruct H as [H].
    contradiction not_conv_rest.
    depelim H.
    depelim a. intros.
    erewrite (abstract_env_ext_irr _ _ wfΣ); eauto.
    constructor; auto.
    split; auto.
    Unshelve. all: eauto.
  Qed.

  Definition isconv_context
            (Γ Γ' Δ Δ' : context)
            (cc : Σ (wfΣ : abstract_env_ext_rel X Σ), Σ Γ = Γ' )
            (check :
                (leq : conv_pb) (Δh : context_hole) (t : term) (Δh' : context_hole) (t' : term),
                 Δ = fill_context_hole Δh t
                 Δ' = fill_context_hole Δh' t'
                 ( Σ (wfΣ : abstract_env_ext_rel X Σ), ws_cumul_ctx_pb_rel Conv Σ Γ (context_hole_context Δh) (context_hole_context Δh'))
                 ConversionResult ( Σ (wfΣ : abstract_env_ext_rel X Σ), conv_cum leq Σ (Γ,,, context_hole_context Δh) t t'))
    : ConversionResult ( Σ (wfΣ : abstract_env_ext_rel X Σ), ws_cumul_ctx_pb_rel Conv Σ Γ Δ Δ') :=
    isconv_context_aux Γ Γ' Δ Δ' cc check Δ Δ' [] [] eq_refl eq_refl.

  Lemma case_conv_brs_inv {Γ ci br br' p c brs1 brs2 π}
  (h : wtp Γ (tCase ci p c (brs1 ++ br :: brs2)) π)
  (p' : predicate term) (c' : term) (brs1' brs2' : list (branch term))
  (π' : stack) (h' : wtp Γ (tCase ci p' c' (brs1' ++ br' :: brs2')) π')
  (hx : conv_stack_ctx Γ π π')
  (hp : Σ (wfΣ : abstract_env_ext_rel X Σ), ws_cumul_pb_predicate Σ (Γ ,,, stack_context π) p p' )
  (h1 : Σ (wfΣ : abstract_env_ext_rel X Σ), ws_cumul_pb_brs Σ (Γ ,,, stack_context π) p brs1 brs1' ) :
   mdecl idecl,
     Σ (wfΣ : abstract_env_ext_rel X Σ), declared_inductive Σ ci mdecl idecl,
       #|pparams p| = ind_npars mdecl,
       #|pparams p'| = ind_npars mdecl,
       eq_context_gen eq eq br.(bcontext) br'.(bcontext),
       test_context_k (fun k : naton_free_vars (closedP k (fun _ : nattrue)))
         #|pparams p| br.(bcontext) &
       test_context_k (fun k : naton_free_vars (closedP k (fun _ : nattrue)))
         #|pparams p'| br'.(bcontext)] .
  Proof using Type.
    destruct (abstract_env_ext_exists X) as [[Σ wfΣ]];
    pose proof ( _ wfΣ) as []. specialize_Σ wfΣ.
    destruct hx as [hx].
    destruct hp as [hp].
    destruct h1 as [h1].
    eapply welltyped_zipc_zipp in h; auto.
    eapply welltyped_zipc_zipp in h'; auto.
    rewrite zipp_as_mkApps in h, h'.
    destruct h as [s h]. destruct h' as [s' h'].
    eapply PCUICValidity.inversion_mkApps in h as [A [hcase _]].
    eapply PCUICValidity.inversion_mkApps in h' as [A' [hcase' _]].
    destruct hp as [].
    eapply inversion_Case in hcase as [mdecl [idecl [decli [indices [hcase _]]]]]; auto.
    eapply inversion_Case in hcase' as [mdecl' [idecl' [decli' [indices' [hcase' _]]]]]; auto.
    destruct (declared_inductive_inj decli decli'). subst mdecl' idecl'.
    constructor.
    assert (clm' : test_context_k (fun k : naton_free_vars (closedP k (fun _ : nattrue)))
      #|pparams p'| br'.(bcontext)).
    { rewrite test_context_k_closed_on_free_vars_ctx.
      destruct hcase'.
      eapply All2i_app_inv_r in brs_ty as (? & ? & ? & ? & ?).
      depelim a2. clear a1 a2.
      destruct p0 as [p0 _].
      cbn in p0.
      eapply PCUICConfluence.eq_context_upto_names_on_free_vars.
      2:symmetry; exact p0.
      rewrite <-closedn_ctx_on_free_vars.
      destruct ci. cbn.
      eapply PCUICClosed.closedn_ctx_upwards.
      { eapply (PCUICInstConv.closedn_ctx_cstr_branch_context (c:=(ci_ind, #|x|)) (idecl:=idecl)).
        split; auto. rewrite e; cbn. rewrite nth_error_app_ge; auto.
        now rewrite Nat.sub_diag; cbn. }
      rewrite (wf_predicate_length_pars wf_pred).
      now rewrite (PCUICGlobalEnv.declared_minductive_ind_npars decli).
    }
    rewrite test_context_k_closed_on_free_vars_ctx.
    destruct hcase.
    eapply All2i_app_inv_r in brs_ty as (? & ? & ? & ? & ?).
    depelim a2. eapply All2i_length in a1; clear a2.
    destruct p0 as [p0 _].
    destruct hcase'.
    eapply All2i_app_inv_r in brs_ty as (? & ? & ? & ? & ?).
    depelim a3. eapply All2i_length in a2. clear a3.
    destruct p1 as [p1 _].
    rewrite e in e0. cbn in ×.
    pose proof (All2_length h1). rewrite <- a1 in H.
    rewrite <- a2 in H. eapply app_inj_length_l in e0 as [-> eq]; auto.
    noconf eq. mdecl, idecl.
    split; tea.
    - intros. erewrite (abstract_env_ext_irr _ _ wfΣ); eauto.
    - eapply (wf_predicate_length_pars wf_pred).
    - eapply (wf_predicate_length_pars wf_pred0).
    - eapply alpha_eq_context_gen. etransitivity; tea.
      now symmetry.
    - eapply PCUICConfluence.eq_context_upto_names_on_free_vars.
      2:symmetry; exact p0.
      rewrite <- closedn_ctx_on_free_vars.
      destruct ci. cbn.
      eapply PCUICClosed.closedn_ctx_upwards.
      { eapply (PCUICInstConv.closedn_ctx_cstr_branch_context (c:=(ci_ind, #|x0|)) (idecl:=idecl)).
        split; auto. rewrite e; cbn. rewrite nth_error_app_ge; auto.
        now rewrite Nat.sub_diag; cbn. }
      rewrite (wf_predicate_length_pars wf_pred).
      now rewrite (PCUICGlobalEnv.declared_minductive_ind_npars decli).
      Unshelve. all: eauto.
  Qed.

  Equations isconv_branches (Γ : context)
    (ci : case_info)
    (p : predicate term) (c : term) (brs1 brs2 : list (branch term))
    (π : stack) (h : wtp Γ (tCase ci p c (brs1 ++ brs2)) π)
    (p' : predicate term) (c' : term) (brs1' brs2' : list (branch term))
    (π' : stack) (h' : wtp Γ (tCase ci p' c' (brs1' ++ brs2')) π')
    (hx : conv_stack_ctx Γ π π')
    (hp : Σ (wfΣ : abstract_env_ext_rel X Σ), ws_cumul_pb_predicate Σ (Γ ,,, stack_context π) p p' )
    (h1 : Σ (wfΣ : abstract_env_ext_rel X Σ), ws_cumul_pb_brs Σ (Γ ,,, stack_context π) p brs1 brs1' )
    (aux : Aux Term Γ (tCase ci p c (brs1 ++ brs2)) π (tCase ci p' c' (brs1' ++ brs2')) π' h')
    : ConversionResult ( Σ (wfΣ : abstract_env_ext_rel X Σ), ws_cumul_pb_brs Σ (Γ ,,, stack_context π) p brs2 brs2' )
    by struct brs2 :=

    isconv_branches Γ ci
      p c brs1 ({| bcontext := m; bbody := br |} :: brs2) π h
      p' c' brs1' ({| bcontext := m'; bbody := br' |} :: brs2') π' h' hx hp h1 aux
     with isconv_red_raw Conv
              br (Case_branch ci p c (brs1, branch_hole_body m, brs2) :: π)
              br' (Case_branch ci p' c' (brs1', branch_hole_body m', brs2') :: π') aux := {
      | Success h2
        with isconv_branches Γ ci
              p c (brs1 ++ [{|bcontext := m; bbody := br|}]) brs2 π _
              p' c' (brs1' ++ [{| bcontext := m'; bbody := br'|}]) brs2' π' _ hx hp _ (expand aux) := {
        | Success h3 := yes ;
        | Error e h'' := no e
        } ;
      | Error e nconv := no e
    } ;

    isconv_branches Γ ci
      p c brs1 [] π h
      p' c' brs1' [] π' h' hx hp h1 aux := yes ;

    isconv_branches Γ ci
      p c brs1 brs2 π h
      p' c' brs1' brs2' π' h' hx hp h1 aux := False_rect _ _.
  Next Obligation.
    constructor. constructor.
  Qed.
  Next Obligation.
    clear aux.
    destruct (abstract_env_ext_exists X) as [[Σ wfΣ]].
    specialize_Σ wfΣ.
    destruct h1 as [h1].
    apply All2_length in h1 as e1.
    apply welltyped_zipc_tCase_brs_length in h as (?&?&?&?); eauto.
    apply welltyped_zipc_tCase_brs_length in h' as (?&?&?&?); eauto.
    pose proof (PCUICInductiveInversion.declared_inductive_unique_sig H H1) as u; noconf u.
    rewrite app_length in ×.
    cbn in ×.
    lia.
  Qed.
  Next Obligation.
    clear aux.
    destruct (abstract_env_ext_exists X) as [[Σ wfΣ]].
    specialize_Σ wfΣ.
    destruct h1 as [h1].
    apply All2_length in h1 as e1.
    apply welltyped_zipc_tCase_brs_length in h as (?&?&?&?); eauto.
    apply welltyped_zipc_tCase_brs_length in h' as (?&?&?&?); eauto.
    pose proof (PCUICInductiveInversion.declared_inductive_unique_sig H H1) as u; noconf u.
    rewrite app_length in ×.
    cbn in ×.
    lia.
  Qed.
  Next Obligation.
    eapply R_positionR. all: simpl.
    1: reflexivity.
    rewrite <- app_nil_r.
    rewrite stack_position_cons.
    eapply positionR_poscat.
    constructor.
  Qed.
  Next Obligation.
    eapply case_conv_brs_inv in h1; tea.
    rename H into wfΣ; pose proof ( _ wfΣ).
    specialize_Σ wfΣ.
    sq. destruct h1 as [mdecl [idecl [decli eqp eqp' eqm clm clm']]].
    transitivity (Γ ,,, stack_context π ,,, inst_case_context (pparams p') (puinst p') m').
    - unfold app_context; rewrite <-app_assoc.
      inv_on_free_vars.
      eapply inst_case_ws_cumul_ctx_pb; tea.
      × fvs.
      × fvs.
      × eapply hp.
      × eapply hp.
    - unfold app_context. rewrite <- app_assoc. eapply ws_cumul_ctx_pb_app_same; auto.
      rewrite on_free_vars_ctx_app.
      apply andb_true_iff. split; auto. 1:now apply ws_cumul_ctx_pb_closed_left in hx.
      eapply on_free_vars_ctx_inst_case_context; trea.
      destruct hp.
      now eapply (ws_cumul_pb_terms_open_terms_right a).
  Qed.
  Next Obligation.
    now rewrite <- app_assoc.
  Qed.
  Next Obligation.
    now rewrite <- app_assoc.
  Qed.
  Next Obligation.
    destruct (case_conv_brs_inv h p' c' brs1' brs2' _ h') as [[mdecl [idecl [decli eqp eqp' eqm clm clm']]]]; tea.
    specialize_Σ wfΣ.
    destruct h1 as [h1], h2 as [h2].
    constructor. apply All2_app.
    - assumption.
    - constructor.
      2: now constructor.
      simpl.
      unfold zipp in h2.
      split; auto.
      cbn in h2.
      unfold inst_case_branch_context. cbn.
      now unfold app_context; rewrite app_assoc.
  Qed.
  Next Obligation.
    clear aux. unfold isconv_branches_obligations_obligation_13.
    eapply R_irrelevance. 2:tea. cbn.
    f_equal. f_equal. 2:{ f_equal. now rewrite <-app_assoc. }
    f_equal. f_equal. f_equal. now rewrite <- app_assoc.
  Qed.
  Next Obligation.
    destruct (case_conv_brs_inv h p' c' brs1' brs2' _ h') as [[mdecl [idecl [decli eqp eqp' eqm clm clm']]]]; tea.
    specialize_Σ wfΣ.
    destruct h2 as [h2], h3 as [h3].
    constructor.
    constructor; auto.
    unfold zipp in *; simpl in ×.
    split; auto.
    rewrite app_context_assoc in h2; auto.
  Qed.
  Next Obligation.
    apply h''; clear h''. intros. specialize_Σ wfΣ.
    destruct H as [H]; inversion H; now constructor.
  Qed.
  Next Obligation.
    apply nconv; clear nconv. intros Σ wfΣ. specialize_Σ wfΣ.
    destruct h1 as [h1], H as [h2].
    constructor. inversion h2; clear h2.
    destruct X0 as [_ h2]. simpl in h2. cbn.
    now rewrite app_context_assoc.
  Qed.

  Equations isconv_branches' (Γ : context)
    (ci : case_info)
    (p : predicate term) (c : term) (brs : list (branch term))
    (π : stack) (h : wtp Γ (tCase ci p c brs) π)
    (ci' : case_info)
    (p' : predicate term) (c' : term) (brs' : list (branch term))
    (π' : stack) (h' : wtp Γ (tCase ci' p' c' brs') π')
    (hx : conv_stack_ctx Γ π π')
    (hp : Σ (wfΣ : abstract_env_ext_rel X Σ), ws_cumul_pb_predicate Σ (Γ ,,, stack_context π) p p' )
    (ei : ci = ci')
    (aux : Aux Term Γ (tCase ci p c brs) π (tCase ci' p' c' brs') π' h')
    : ConversionResult ( Σ (wfΣ : abstract_env_ext_rel X Σ), ws_cumul_pb_brs Σ (Γ ,,, stack_context π) p brs brs' ) :=

    isconv_branches' Γ ci p c brs π h ci' p' c' brs' π' h' hx hp eci aux :=
      isconv_branches Γ ci p c [] brs π _ p' c' [] brs' π' _ _ _ _ (expand aux).
  Next Obligation.
    constructor. constructor.
  Qed.

  Inductive fix_kind :=
  | IndFix
  | CoIndFix.

  Definition mFix k :=
    match k with
    | IndFixtFix
    | CoIndFixtCoFix
    end.

  Definition mFix_mfix fk :=
    match fk with
    | IndFixFix
    | CoIndFixCoFix
    end.

  Definition mFixRargMismatch fk :=
    match fk with
    | IndFixFixRargMismatch
    | CoIndFixCoFixRargMismatch
    end.

  Definition mFixMfixMismatch fk :=
    match fk with
    | IndFixFixMfixMismatch
    | CoIndFixCoFixMfixMismatch
    end.

  Equations isws_cumul_pb_fix_types (fk : fix_kind) (Γ : context)
    (idx : nat)
    (mfix1 mfix2 : mfixpoint term) (π : stack)
    (h : wtp Γ (mFix fk (mfix1 ++ mfix2) idx) π)
    (mfix1' mfix2' : mfixpoint term) (π' : stack)
    (h' : wtp Γ (mFix fk (mfix1' ++ mfix2') idx) π')
    (hx : conv_stack_ctx Γ π π')
    (h1 : All2 (fun u v
                   ( Σ (wfΣ : abstract_env_ext_rel X Σ), Σ ;;; Γ ,,, stack_context π u.(dtype) = v.(dtype)) ×
                   (u.(rarg) = v.(rarg)) × eq_binder_annot u.(dname) v.(dname)
            ) mfix1 mfix1' )
    (aux : Aux Term Γ (mFix fk (mfix1 ++ mfix2) idx) π (mFix fk (mfix1' ++ mfix2') idx) π' h')
    : ConversionResult ( All2 (fun u v
          ( Σ (wfΣ : abstract_env_ext_rel X Σ), Σ ;;; Γ ,,, stack_context π u.(dtype) = v.(dtype)) ×
          (u.(rarg) = v.(rarg)) × eq_binder_annot u.(dname) v.(dname)
      ) mfix2 mfix2' )
    by struct mfix2 :=

    isws_cumul_pb_fix_types
      fk Γ idx mfix1 (u :: mfix2) π h mfix1' (v :: mfix2') π' h' hx h1 aux
    with inspect (eqb u.(rarg) v.(rarg)) := {
    | @exist true eq1
      with inspect (eqb_binder_annot u.(dname) v.(dname)) := {
      | @exist true eqann
        with isconv_red_raw Conv
             u.(dtype)
             (mFix_mfix fk (mfix1, def_hole_type u.(dname) u.(dbody) u.(rarg), mfix2) idx :: π)
             v.(dtype)
             (mFix_mfix fk (mfix1', def_hole_type v.(dname) v.(dbody) v.(rarg), mfix2') idx :: π')
             aux
      := {
      | Success h2 with
          isws_cumul_pb_fix_types fk Γ idx
            (mfix1 ++ [u]) mfix2 π _
            (mfix1' ++ [v]) mfix2' π' _
            hx _ (expand aux)
        := {
        | Success h3 := yes ;
        | Error e h'' := no e
        } ;
      | Error e h'' := no e
      } ;
      | @exist false neqann := no (
        FixRargMismatch idx
          (Γ ,,, stack_context π) u mfix1 mfix2
          (Γ ,,, stack_context π') v mfix1' mfix2'
      ) };
    | @exist false eq1 := no (
        mFixRargMismatch fk idx
          (Γ ,,, stack_context π) u mfix1 mfix2
          (Γ ,,, stack_context π') v mfix1' mfix2'
      )
    } ;

    isws_cumul_pb_fix_types fk Γ idx mfix1 [] π h mfix1' [] π' h' hx h1 aux := yes ;

    
    isws_cumul_pb_fix_types fk Γ idx mfix1 mfix2 π h mfix1' mfix2' π' h' hx h1 aux :=
      no (
        mFixMfixMismatch fk idx
          (Γ ,,, stack_context π) (mfix1 ++ mfix2)
          (Γ ,,, stack_context π') (mfix1' ++ mfix2')
      ).

  Next Obligation.
    destruct H as [H]; inversion H.
  Qed.
  Next Obligation.
    destruct H as [H]; inversion H.
  Qed.
  Next Obligation.
    destruct u. destruct fk. all: eauto.
  Qed.
  Next Obligation.
    destruct v. destruct fk. all: eauto.
  Qed.
  Next Obligation.
    eapply R_positionR. all: simpl.
    - destruct u. destruct fk. all: reflexivity.
    - rewrite <- app_nil_r, stack_position_cons. destruct fk.
      + eapply positionR_poscat. constructor.
      + eapply positionR_poscat. constructor.
  Qed.
  Next Obligation.
    destruct fk.
    - simpl. eauto.
    - simpl. eauto.
  Qed.
  Next Obligation.
    rewrite <- app_assoc. simpl. eauto.
  Qed.
  Next Obligation.
    rewrite <- app_assoc. simpl. eauto.
  Qed.
  Next Obligation.
    destruct (abstract_env_ext_exists X) as [[Σ wfΣ]].
    specialize_Σ wfΣ.
    destruct hx as [hx], h1 as [h1], h2 as [h2].
    destruct ( _ wfΣ) as [].
    unfold zipp in h2.
    constructor.
    apply All2_app. 1: assumption.
    constructor. 2: constructor.
    change (true = eqb u.(rarg) v.(rarg)) in eq1.
    destruct (eqb_specT u.(rarg) v.(rarg)). 2: discriminate.
    symmetry in eqann.
    apply eqb_binder_annot_spec in eqann.
    split; auto.
    destruct fk; simpl in *; auto.
    all: intros; erewrite (abstract_env_ext_irr _ _ wfΣ); intuition eauto.
    Unshelve. all: eauto.
  Qed.
  Next Obligation.
    clear aux.
    eapply R_irrelevance; tea; cbn.
    now rewrite <- !app_assoc.
  Qed.
  Next Obligation.
    destruct (abstract_env_ext_exists X) as [[Σ wfΣ]].
    specialize_Σ wfΣ.
    destruct hx as [hx], h1 as [h1], h2 as [h2].
    destruct ( _ wfΣ) as [].
    unfold zipp in h2. sq.
    constructor.
    2: eauto.
    change (true = eqb u.(rarg) v.(rarg)) in eq1.
    destruct (eqb_specT u.(rarg) v.(rarg)). 2: discriminate.
    symmetry in eqann.
    apply eqb_binder_annot_spec in eqann.
    clear eq1.
    destruct fk.
    all: split; [ intros; erewrite (abstract_env_ext_irr _ _ wfΣ) | ]; intuition eauto .
    Unshelve. all: eauto.
  Qed.
  Next Obligation.
    apply h''; clear h''.
    destruct H as [H]; inversion H.
    constructor; assumption.
  Qed.
  Next Obligation.
    destruct (abstract_env_ext_exists X) as [[Σ wfΣ]].
    specialize_Σ wfΣ.
    destruct H as [H]; inversion H; destruct X0 as [eq_uv _].
    apply h''; clear h''; constructor.
    destruct fk; apply eq_uv; eauto.
  Qed.
  Next Obligation.
    destruct (abstract_env_ext_exists X) as [[Σ wfΣ]].
    specialize_Σ wfΣ.
    destruct H as [H]; inversion H; destruct X0 as [_ [eq_uv eqann]].
    change (?ru =? ?rv) with (eqb ru rv) in eq1.
    symmetry in neqann.
    pose proof (eqb_annot_reflect (dname u) (dname v)) as r.
    now apply (ssrbool.elimF r neqann).
  Qed.
  Next Obligation.
    destruct (abstract_env_ext_exists X) as [[Σ wfΣ]].
    specialize_Σ wfΣ.
    destruct H as [H]; inversion H; destruct X0 as [_ [eq_uv eqann]].
    change (?ru =? ?rv) with (eqb ru rv) in eq1.
    destruct (eqb_specT (rarg u) (rarg v)) as [|neq_uv]; [discriminate|].
    exact (neq_uv eq_uv).
  Qed.

  Lemma conv_context_decl Pcmp :
     Σ Γ Δ d d',
      conv_context Pcmp Σ Γ Δ
      conv_decls Pcmp Σ Γ Δ d d'
      conv_context Pcmp Σ (Γ ,, d) (Δ ,, d').
  Proof using Type.
    intros Γ Δ d d' hx h.
    destruct h.
    all: constructor. all: try assumption.
    all: constructor. all: assumption.
  Qed.

  Lemma stack_entry_context_mFix_mfix_bd :
     fk na ty ra mfix1 mfix2 idx,
      stack_entry_context (mFix_mfix fk (mfix1, def_hole_body na ty ra, mfix2) idx) =
      fix_context_alt (map def_sig mfix1 ++ (na,ty) :: map def_sig mfix2).
  Proof using Type.
    intros fk na ty ra mfix1 mfix2 idx.
    destruct fk. all: reflexivity.
  Qed.

  Equations isws_cumul_pb_fix_bodies (fk : fix_kind) (Γ : context) (idx : nat)
    (mfix1 mfix2 : mfixpoint term) (π : stack)
    (h : wtp Γ (mFix fk (mfix1 ++ mfix2) idx) π)
    (mfix1' mfix2' : mfixpoint term) (π' : stack)
    (h' : wtp Γ (mFix fk (mfix1' ++ mfix2') idx) π')
    (hx : conv_stack_ctx Γ π π')
    (h1 : All2 (fun u v Σ (wfΣ : abstract_env_ext_rel