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 . 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 \ 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 [] []; 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 [] []; 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 [[] []]]]]; 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 [[q'' h] ?].
          unfold R_aux_obligations_obligation_2.
          simpl. f_equal. f_equal.
          eapply uip.
        × intros [ ] [ ] e [[ ] ] [[ ] ] h.
          destruct e as [e'].
          simpl in ×.
          dependent destruction h.
          -- left. unfold posR in ×. simpl in ×. assumption.
          -- match goal with
             | |- context [ exist ? ] ⇒
               assert (ee : = ) by eapply uip
             end.
            rewrite ee. right. clear ee. assumption.
        × eapply wcored_wf.
    - intros x x' y [e] [y' [x'' [r [[] []]]]]; 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 [[q' h] [? [? ?]]].
      unfold R_aux_obligations_obligation_1.
      simpl. f_equal. f_equal.
      eapply uip.
    - intros x x' e
             [[ ] [[u hu] [[ ] ]]]
[[ ] [[v hv] [[ ] ]]] hl.
      destruct e as [e']; eauto.
      simpl in ×.
      dependent destruction hl.
      + left. unfold posR in ×.
        simpl in ×.
        assumption.
      + match goal with
        | |- context [ exist ? ] ⇒
          assert (ee : = ) 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 := t Σ, abstract_env_ext_rel X Σ welltyped Σ _ t)
                                 _ ( Σ 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 := 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 ( xpos x × state) (` x.π2.2.π1) x.π2.2.π2)) =
    ((y.π1; y.π2.1), (existT ( 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 . destruct w as [w wt], w' as [w' wt'].
    cbn in ×. subst w'. noconf .
    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 . 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 ) (pzt ))
      R Γ .
  Proof using Type.
    intros Γ h.
    left. intros. eapply cored_cored'. eapply h; eauto.
  Qed.


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


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


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


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


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


  Lemma R_positionR2 :
     Γ p1 p2,
      (eqt (pzt ) (pzt ))
      ` (pps1 ) = ` (pps1 )
      (eqt (` (pwt )) (` (pwt )))
      positionR (` (pps2 )) (` (pps2 ))
      R Γ .
  Proof using Type.
    intros Γ [ π1 ρ1 ] [ π2 ρ2 ] h.
    simpl in ×.
    eapply R_aux_positionR2. all: simpl. all: auto.
  Qed.


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


  Lemma R_stateR :
     Γ p1 p2,
      (eqt (pzt ) (pzt ))
      ` (pps1 ) = ` (pps1 )
      (eqt (` (pwt )) (` (pwt )))
      ` (pps2 ) = ` (pps2 )
      stateR (st ) (st )
      R Γ .
  Proof using Type.
    intros Γ [ π1 ρ1 ] [ π2 ρ2 ] 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 π1) (zipp π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 Γ π1')
       (h2' : wtp Γ π2'),
       conv_stack_ctx Γ π1 π2
       R Γ
         (mkpack Γ s' π1' π2' )
         (mkpack Γ s π1 π2 )
       Ret s' Γ π1' π2'.

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

  Local Notation yes := (Success _) (only parsing).
  Local Notation no := ( 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 π1 π2 aux :=
    (aux Reduction π1 π2 _ _ _ _ leq _ I I I) (only parsing).
  Notation isconv_prog_raw leq π1 π2 aux :=
    (aux Term π1 π2 _ _ _ _ leq _ _ _ I) (only parsing).
  Notation isconv_args_raw leq π1 π2 aux :=
    (aux Args π1 π2 _ _ _ _ leq _ I I I) (only parsing).
  Notation isconv_fallback_raw leq π1 π2 aux :=
    (aux Fallback π1 π2 _ _ _ _ leq _ _ _ _) (only parsing).

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

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

    _isconv_red Γ leq π1 π2 hx aux
    with inspect (decompose_stack π1) := {
    | @exist (, ρ1) with inspect (decompose_stack π2) := {
      | @exist (, ρ2)
        with inspect (reduce_stack RedFlags.nodelta _ X
                                   (Γ ,,, stack_context π1)
                                    (appstack []) _) := {
        | @exist (,π1')
          with inspect (reduce_stack RedFlags.nodelta _ X
                                     (Γ ,,, stack_context π2)
                                      (appstack []) _) := {
          | @exist (,π2') isconv_prog leq (π1' ρ1) (π2' ρ2) aux
          }
        }
      }
    }.
  Next Obligation.
    symmetry in .
    pose proof (heΣ _ wfΣ); sq.
    eapply welltyped_zipc_stack_context ; eauto.
  Qed.
  Next Obligation.
    clear aux .
    symmetry in .
    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 .
    - 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 with
    | _ = reduce_stack ?f ?Σ ?X ?Γ ?t ?π ?h
      pose proof (reduce_stack_decompose RedFlags.nodelta _ X _ _ _ h) as ;
      pose proof (reduce_stack_context f Σ X Γ t π h) as
    end.
    rewrite in . cbn in .
    rewrite in . cbn in .
    rewrite stack_context_appstack in . cbn in .
    pose proof (decompose_stack_eq _ _ _ (eq_sym )). subst.
    destruct (abstract_env_ext_exists X) as [[Σ wfΣ]].
    match type of with
    | _ = reduce_stack ?f _ ?X ?Γ ?t ?π ?hh
      pose proof (reduce_stack_Req f _ X _ wfΣ _ _ _ hh) as [ e | h ]
    end.
     - assert ( := ). rewrite e in . inversion . subst.
      match type of with
      | _ = reduce_stack ?f ?Σ ?X ?Γ ?t ?π ?h
        pose proof (reduce_stack_decompose RedFlags.nodelta _ X _ _ _ h) as ;
        pose proof (reduce_stack_context f Σ X Γ t π h) as
      end.
      rewrite in . cbn in .
      rewrite in . cbn in .
      rewrite stack_context_appstack in . cbn in .
      pose proof (decompose_stack_eq _ _ _ (eq_sym )). subst.
      match type of with
      | _ = reduce_stack ?f _ ?X ?Γ ?t ?π ?hh
        pose proof (reduce_stack_Req f _ X Σ wfΣ _ _ _ hh) as [ ee | h ]
      end.
      + assert ( := ). rewrite ee in . inversion . 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 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 . inversion . 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 .
             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 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 . inversion .         subst.
        unshelve eapply R_positionR ; simpl.
        × f_equal.
          rewrite zipc_stack_cat.
          rewrite .
          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 ( 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 : ) (π : 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)) with inspect (decompose_stack_at π arg) := {
      | @exist (Some (l, c, θ)) with inspect (reduce_stack RedFlags.default _ X
                                                               (Γ ,,, stack_context θ) c [] _) := {
        | @exist (cred, ρ) 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 .
    pose proof (decompose_stack_at_eq _ _ _ _ _ ). 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 ) 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 with
    | _ = reduce_stack ?flags _ ?X ?Γ ?t ?π ?h
      pose proof (reduce_stack_sound flags _ X Σ wfΣ Γ t π h) as [] ;
      pose proof (reduce_stack_decompose flags _ X Γ t π h) as hd
    end.
    rewrite in . cbn in .
    rewrite 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 .
    rewrite stack_context_appstack.
    eapply trans_red.
    - eapply red_app_r. exact .
    - 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 ) as eql.
        apply decompose_stack_at_length in eql. subst.
        rewrite nth_error_app_ge by auto.
        replace (#|l| - #|l|) with 0 by . cbn.
        case_eq (decompose_stack ρ). intros 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 ) 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 with
    | _ = reduce_stack ?flags _ ?X ?Γ ?t ?π ?h
      pose proof (reduce_stack_sound flags _ X Σ wfΣ Γ t π h) as [] ;
      pose proof (reduce_stack_decompose flags _ X Γ t π h) as hd
    end.
    rewrite in . cbn in .
    rewrite 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 .
    eapply trans_red.
    - eapply red_app_r. exact .
    - 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 ) as eql.
        apply decompose_stack_at_length in eql. subst.
        rewrite nth_error_app_ge by auto.
        replace (#|l| - #|l|) with 0 by . cbn.
        case_eq (decompose_stack ρ). intros 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 ) as eq.
    pose proof (decompose_stack_at_eq _ _ _ _ _ eq). subst.
    rewrite !zipc_appstack. cbn.
    match type of with
    | _ = reduce_stack ?flags _ ?X ?Γ ?t ?π ?h
      pose proof (reduce_stack_sound flags _ X Σ wfΣ Γ t π h) as [] ;
      pose proof (reduce_stack_decompose flags _ X Γ t π h) as hd
    end.
    clear . cbn in .
    rewrite in . cbn in .
    rewrite in hd. cbn in hd.
    do 2 zip fold. constructor. eapply red_context_zip.
    eapply trans_red.
    - eapply red_app_r. exact .
    - 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 ) as eql.
        apply decompose_stack_at_length in eql. subst.
        rewrite nth_error_app_ge by auto.
        replace (#|l| - #|l|) with 0 by . cbn.
        case_eq (decompose_stack ρ). intros 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 ) as eq.
    pose proof (decompose_stack_at_eq _ _ _ _ _ eq). subst.
    rewrite !zipc_appstack. cbn.
    match type of with
    | _ = reduce_stack ?flags _ ?X ?Γ ?t ?π ?h
      pose proof (reduce_stack_sound flags _ X Σ wfΣ Γ t π h) as [] ;
      pose proof (reduce_stack_decompose flags _ X Γ t π h) as hd
    end.
    rewrite in . cbn in .
    rewrite in hd. cbn in hd.
    do 2 zip fold. eapply cored_context.
    eapply cored_red_trans.
    - eapply red_app_r. exact .
    - 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 ) as eql.
        apply decompose_stack_at_length in eql. subst.
        rewrite nth_error_app_ge by auto.
        replace (#|l| - #|l|) with 0 by . cbn.
        case_eq (decompose_stack ρ). intros 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 ) as eq.
    pose proof (decompose_stack_at_eq _ _ _ _ _ eq). subst.
    rewrite 2!decompose_stack_appstack. cbn.
    case_eq (decompose_stack θ). intros .
    reflexivity.
  Qed.


  Lemma unfold_one_fix_None Γ mfix idx π wf :
    None = unfold_one_fix Γ mfix idx π wf
    args,
      Σ (wfΣ : abstract_env_ext_rel X Σ),
       (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 .
      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 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 in r, wh, decomp, isr.
      specialize (isr eq_refl) as (noapp&_).
      cbn in ×.
      clear H .
      destruct (heΣ Σ wfΣ).
      symmetry in .
      apply decompose_stack_at_length in as ?.
      apply decompose_stack_at_eq in 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 ) :: (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 ) (tApp )

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

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

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

  | 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 ) (tApp ) :=
      prog_view_App ;

    prog_viewc (tConst ) (tConst ) :=
      prog_view_Const ;

    prog_viewc (tLambda ) (tLambda ) :=
      prog_view_Lambda ;

    prog_viewc (tProd ) (tProd ) :=
      prog_view_Prod ;

    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 ; eauto.
  Qed.


  Definition eqb_universe_instance_gen eq u v :=
     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 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 )
    : ConversionResult (conv_term leq Γ (tConst c u) π1 (tConst c' u') π2) :=

    unfold_constants Γ leq c u π1 c' u' π2 ne hx aux
    with inspect (abstract_env_lookup X c') := {
    | @exist (Some (ConstantDecl {| cst_body := Some b |})) :=
      isconv_red leq (tConst c u) π1 (subst_instance u' b) π2 aux ;
    
    | @exist _ with inspect (abstract_env_lookup X c) := {
      | @exist (Some (ConstantDecl {| cst_body := Some b |})) :=
        isconv_red leq (subst_instance u b) π1
                        (tConst c' u') π2 aux ;
      
      | @exist _ := no (NotFoundConstants c c')
      }
    }.
  Ltac solve_unfold_constants aux Σ wfΣ :=
  try destruct (abstract_env_ext_exists X) as [[Σ wfΣ]];
  exfalso;
  Tactics.program_simplify;
  CoreTactics.equations_simpl;
  try erewrite abstract_env_lookup_correct in ; eauto ;
  try erewrite abstract_env_lookup_correct in ; 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 .
    pose proof ( _ wfΣ).
    sq.
    eapply red_welltyped; try eapply ; 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 ; eauto.
      eapply welltyped_is_open_term in .
      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 ; eauto.
      eapply welltyped_is_open_term in . 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 ( _ 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 ; 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 ; 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 [(?&?&[ eq])]; auto.
    2: pose proof ( _ wfΣ); sq ; eauto.
    rewrite zipp_as_mkApps in , .
    erewrite abstract_env_lookup_correct in , ; eauto.
    symmetry in , .
    generalize . intros []; eauto.
    unshelve eapply closed_red_mkApps_tConst_axiom in as (?&&?); eauto.
    eapply closed_red_mkApps_tConst_axiom in as (?&&?); eauto.
    apply eq_termp_mkApps_inv in eq as (eq&?); [|easy|easy].
    depelim eq.
    destruct ne as [|(_&ne)]; [congruence|].

    clear aux. specialize ( _ wfΣ). specialize ( _ wfΣ).
    apply welltyped_zipc_tConst_inv in as (&&); eauto.
    apply welltyped_zipc_tConst_inv in as (&&); eauto.
    eapply declared_constant_inj in ; eauto; subst.
    apply consistent_instance_ext_wf in .
    apply consistent_instance_ext_wf in .
    eapply eqb_universe_instance_complete in r; auto.
  Qed.
  Next Obligation. solve_unfold_constants aux Σ wfΣ. Qed.
  Next Obligation. solve_unfold_constants aux Σ wfΣ. Qed.
  Next Obligation. solve_unfold_constants aux Σ wfΣ. Qed.
  Next Obligation. solve_unfold_constants aux Σ wfΣ. Qed.
  Next Obligation. solve_unfold_constants aux Σ H. Qed.
  Next Obligation. solve_unfold_constants aux Σ wfΣ. Qed.
  Next Obligation. solve_unfold_constants aux Σ wfΣ. Qed.
  Next Obligation. solve_unfold_constants aux Σ wfΣ. Qed.
  Next Obligation. solve_unfold_constants aux Σ wfΣ. Qed.
  Next Obligation. solve_unfold_constants aux Σ wfΣ. Qed.
  Next Obligation. solve_unfold_constants aux Σ wfΣ. Qed.
  Next Obligation. solve_unfold_constants aux Σ H. Qed.
  Next Obligation. solve_unfold_constants aux Σ wfΣ. Qed.
  Next Obligation. solve_unfold_constants aux Σ wfΣ. Qed.
  Next Obligation. solve_unfold_constants aux Σ wfΣ. Qed.
  Next Obligation. solve_unfold_constants aux Σ 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' : Δ' = ,,, ) :
    ConversionResult ( Σ (wfΣ : abstract_env_ext_rel X Σ), ws_cumul_ctx_pb_rel Conv Σ Γ Δpre ) by struct Δpre := {

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

    isconv_context_aux Γ Γ' Δ Δ' cc check
                           (mkdecl na bd ty :: Δpre)
                           (mkdecl na' bd' ty' :: )
                           Δpost eq eq'
      with isconv_context_aux
             Γ Γ' Δ Δ' cc check Δpre
             (Δpost [mkdecl na bd ty])
             ( [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)
                                           (Γ',,, ) (mkdecl na' bd' ty'));

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

          | Error ce not_conv_typeno (ContextNotConvertibleType
                                            (Γ,,, Δpre) (mkdecl na bd ty)
                                            (Γ',,, ) (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
                     (, decl_hole_body na' ty', ) body'
                     _ _ conv_rest := {
              | Error ce not_conv_bodyno (ContextNotConvertibleBody
                                                (Γ,,, Δpre) (mkdecl na bd ty)
                                                (Γ',,, ) (mkdecl na' bd' ty'));
              
              | Success conv_bodyyes
              };

            | None | Noneyes;

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

    isconv_context_aux Γ Γ' Δ Δ' cc check
                       Δpre Δ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 . 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 .
  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 .
  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 ; 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 .
    - 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 ( br :: )) π)
  (p' : predicate term) (c' : term) (brs1' brs2' : list (branch term))
  (π' : stack) (h' : wtp Γ (tCase ci p' c' ( br' :: )) π')
  (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 ) :
   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 ( k : on_free_vars (closedP k ( _ : true)))
         #|pparams p| br.(bcontext) &
       test_context_k ( k : on_free_vars (closedP k ( _ : true)))
         #|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 as [].
    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 ( k : on_free_vars (closedP k ( _ : true)))
      #|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 . clear .
      destruct as [ _].
      cbn in .
      eapply PCUICConfluence.eq_context_upto_names_on_free_vars.
      2:symmetry; exact .
      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 . eapply All2i_length in ; clear .
    destruct as [ _].
    destruct hcase'.
    eapply All2i_app_inv_r in brs_ty as (? & ? & ? & ? & ?).
    depelim . eapply All2i_length in . clear .
    destruct as [ _].
    rewrite e in . cbn in ×.
    pose proof (All2_length ). rewrite in H.
    rewrite in H. eapply app_inj_length_l in 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 .
      rewrite closedn_ctx_on_free_vars.
      destruct ci. cbn.
      eapply PCUICClosed.closedn_ctx_upwards.
      { eapply (PCUICInstConv.closedn_ctx_cstr_branch_context (c:=(ci_ind, #||)) (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 ( )) π)
    (p' : predicate term) (c' : term) (brs1' brs2' : list (branch term))
    (π' : stack) (h' : wtp Γ (tCase ci p' c' ( )) π')
    (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 )
    (aux : Aux Term Γ (tCase ci p c ( )) π (tCase ci p' c' ( )) π' h')
    : ConversionResult ( Σ (wfΣ : abstract_env_ext_rel X Σ), ws_cumul_pb_brs Σ (Γ ,,, stack_context π) p )
    by struct :=

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

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

    isconv_branches Γ ci
      p c π h
      p' c' π' h' hx hp aux := False_rect _ _.
  Next Obligation.
    constructor. constructor.
  Qed.
  Next Obligation.
    clear aux.
    destruct (abstract_env_ext_exists X) as [[Σ wfΣ]].
    specialize_Σ wfΣ.
    destruct as [].
    apply All2_length in as .
    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 ) as u; noconf u.
    rewrite app_length in ×.
    cbn in ×.
    .
  Qed.
  Next Obligation.
    clear aux.
    destruct (abstract_env_ext_exists X) as [[Σ wfΣ]].
    specialize_Σ wfΣ.
    destruct as [].
    apply All2_length in as .
    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 ) as u; noconf u.
    rewrite app_length in ×.
    cbn in ×.
    .
  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 ; tea.
    rename H into wfΣ; pose proof ( _ wfΣ).
    specialize_Σ wfΣ.
    sq. destruct 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' _ h') as [[mdecl [idecl [decli eqp eqp' eqm clm clm']]]]; tea.
    specialize_Σ wfΣ.
    destruct as [], as [].
    constructor. apply All2_app.
    - assumption.
    - constructor.
      2: now constructor.
      simpl.
      unfold zipp in .
      split; auto.
      cbn in .
      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' _ h') as [[mdecl [idecl [decli eqp eqp' eqm clm clm']]]]; tea.
    specialize_Σ wfΣ.
    destruct as [], as [].
    constructor.
    constructor; auto.
    unfold zipp in *; simpl in ×.
    split; auto.
    rewrite app_context_assoc in ; 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 as [], H as [].
    constructor. inversion ; clear .
    destruct as [_ ]. simpl in . 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 : )
    (mfix1 mfix2 : mfixpoint term) (π : stack)
    (h : wtp Γ (mFix fk ( ) idx) π)
    (mfix1' mfix2' : mfixpoint term) (π' : stack)
    (h' : wtp Γ (mFix fk ( ) idx) π')
    (hx : conv_stack_ctx Γ π π')
    (h1 : ( 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)
            ) )
    (aux : Aux Term Γ (mFix fk ( ) idx) π (mFix fk ( ) idx) π' h')
    : ConversionResult ( ( 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)
      ) )
    by struct :=

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

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

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

  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], as [], as [].
    destruct ( _ wfΣ) as [].
    unfold zipp in .
    constructor.
    apply All2_app. 1: assumption.
    constructor. 2: constructor.
    change (true = eqb u.(rarg) v.(rarg)) in .
    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], as [], as [].
    destruct ( _ wfΣ) as [].
    unfold zipp in . sq.
    constructor.
    2: eauto.
    change (true = eqb u.(rarg) v.(rarg)) in .
    destruct (eqb_specT u.(rarg) v.(rarg)). 2: discriminate.
    symmetry in eqann.
    apply eqb_binder_annot_spec in eqann.
    clear .
    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 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 as [_ [eq_uv eqann]].
    change (?ru =? ?rv) with (eqb ru rv) in .
    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 as [_ [eq_uv eqann]].
    change (?ru =? ?rv) with (eqb ru rv) in .
    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 (, def_hole_body na ty ra, ) idx) =
      fix_context_alt (map def_sig (na,ty) :: map def_sig ).
  Proof using Type.
    intros fk na ty ra idx.
    destruct fk. all: reflexivity.
  Qed.


  Equations isws_cumul_pb_fix_bodies (fk : fix_kind) (Γ : context) (idx : )
    (mfix1 mfix2 : mfixpoint term) (π : stack)
    (h : wtp Γ (mFix fk ( ) idx) π)
    (mfix1' mfix2' : mfixpoint term) (π' : stack)
    (h' : wtp Γ (mFix fk ( ) idx) π')
    (hx : conv_stack_ctx Γ π π')
    (h1 : ( u v Σ (wfΣ : abstract_env_ext_rel X Σ), Σ ;;; Γ ,,, stack_context π ,,, fix_context_alt (map def_sig map def_sig ) u.(dbody) = v.(dbody)) )
    (ha : ( 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)
           ) ( ) ( ) )
    (aux : Aux Term Γ (mFix fk ( ) idx) π (mFix fk ( ) idx) π' h')
    : ConversionResult ( ( u v Σ (wfΣ : abstract_env_ext_rel X Σ), Σ ;;; Γ ,,, stack_context π ,,, fix_context_alt (map def_sig map def_sig ) u.(dbody) = v.(dbody)) )
    by struct :=

  isws_cumul_pb_fix_bodies fk Γ idx (u :: ) π h (v :: ) π' h' hx ha aux
  with isconv_red_raw Conv
        u.(dbody)
        (mFix_mfix fk (, def_hole_body u.(dname) u.(dtype) u.(rarg), ) idx :: π)
        v.(dbody)
        (mFix_mfix fk (, def_hole_body v.(dname) v.(dtype) v.(rarg), ) idx :: π')
        aux
  := {
  | Success
    with isws_cumul_pb_fix_bodies fk Γ idx
           ( [u]) π _
           ( [v]) π' _
           hx _ _ (expand aux)
    := {
    | Success := yes ;
    | Error e h'' := no e
    } ;
  | Error e h'' := no e
  } ;

  isws_cumul_pb_fix_bodies fk Γ idx [] π h [] π' h' hx ha aux := yes ;

  isws_cumul_pb_fix_bodies fk Γ idx π h π' h' hx ha aux :=
    False_rect _ _.

  Next Obligation.
    destruct as [], ha as [ha].
    apply All2_length in as .
    apply All2_length in ha as ea.
    rewrite !app_length in ea. simpl in ea. .
  Qed.
  Next Obligation.
    destruct as [], ha as [ha].
    apply All2_length in as .
    apply All2_length in ha as ea.
    rewrite !app_length in ea. simpl in ea. .
  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.
    rename H into wfΣ; specialize_Σ wfΣ.
    destruct ( _ wfΣ) as [], ha as [ha], hx as [hx].
    clear - wfΣ ha hx. constructor.
    rewrite 2!stack_entry_context_mFix_mfix_bd.
    change (dname u, dtype u) with (def_sig u).
    change (dname v, dtype v) with (def_sig v).
    repeat match goal with
    | |- context [ ?f ?x :: map ?f ?l ] ⇒
      change (f x :: map f l) with (map f (x :: l))
    end.
    rewrite 2!map_app.
    revert ha.
    generalize ( u :: ). intro Δ.
    generalize ( v :: ). intro Δ'.
    intro ha.
    rewrite !app_context_assoc.
    revert hx ha.
    generalize (Γ ,,, stack_context π').
    generalize (Γ ,,, stack_context π).
    clear Γ. intros Γ Γ' hx ha.
    assert (h :
      
        ( d d'(Σ ;;; Γ d.2 = d'.2) × eq_binder_annot d.1 d'.1)
        (map def_sig Δ) (map def_sig Δ')
    ).
    { apply All2_map. eapply All2_impl. 1: eassumption.
      intros [na ty bo ra] [na' ty' bo' ra'] [? [? ?]].
      specialize (w _ wfΣ). simpl in ×. split; tas.
    }
    clear ha.
    revert h.
    generalize (map def_sig Δ). clear Δ. intro Δ.
    generalize (map def_sig Δ'). clear Δ'. intro Δ'.
    intro h.
    unfold fix_context_alt.
    match goal with
    | |- ws_cumul_ctx_pb _ _ (_ ,,, List.rev ?l) (_ ,,, List.rev ?l') ⇒
      assert (hi :
        All2i ( i d d'
           Ξ,
            is_closed_context (Γ ,,, Ξ)
            #|Ξ| = i
            ws_cumul_decls Conv Σ (Γ ,,, Ξ) d d'
        ) 0 l l'
      )
    end.
    { eapply All2i_mapi.
      generalize 0 at 3. intro n.
      induction h in n |- ×. 1: constructor.
      constructor. 2: eapply IHh.
      destruct r.
      intros Ξ cl . constructor; tas.
      rewrite .
      eapply @weakening_ws_cumul_pb with (Γ' := []). all: try assumption.

    }
    clear h.
    revert hi.
    match goal with
    | |- context [ ws_cumul_ctx_pb _ _ (_ ,,, List.rev ?l) (_ ,,, List.rev ?l') ] ⇒
      generalize l' ;
      generalize l
    end.
    clear Δ Δ'. intros Δ Δ' h.
    apply All2i_rev in h. simpl in h.
    revert h.
    rewrite (List.rev_length Δ).
    generalize (List.rev Δ). clear Δ. intro Δ.
    generalize (List.rev Δ'). clear Δ'. intro Δ'.
    intro h.
    set (ln := #|Δ|) in ×.
    set (m := 0) in ×.
    assert (e : ln - m = #|Δ|) by .
    clearbody ln m.
    induction h.
    - eauto.
    - simpl in ×.
      forward IHh by .
      constructor.
      + eapply IHh.
      + eapply . 2:.
        clear - IHh. fvs.
  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], as [], as [], ha as [ha].
    destruct ( _ wfΣ) as [].
    unfold zipp in .     constructor.
    apply All2_app.
    - eapply All2_impl. 1: exact .
      simpl. intros [? ? ? ?] [? ? ? ?] hh.
      simpl in ×.
      rewrite map_app. simpl.
      rewrite !app_assoc. simpl.
      assumption.
    - constructor. 2: constructor.
      rewrite map_app. simpl.
      rewrite !app_assoc. simpl.
      destruct u as [na ty bo ra], v as [na' ty' bo' ra']. simpl in ×.
      unfold def_sig at 2. simpl.
      destruct fk.
      + intros. erewrite (abstract_env_ext_irr _ _ wfΣ); eauto.
       rewrite app_context_assoc in ; eauto.
       + intros. erewrite (abstract_env_ext_irr _ _ wfΣ); eauto.
       rewrite app_context_assoc in ; eauto.
    Unshelve. all: eauto.
  Qed.
  Next Obligation.
    destruct (abstract_env_ext_exists X) as [[Σ wfΣ]].
    specialize_Σ wfΣ.
    destruct ha as [ha].
    constructor.
    rewrite !app_assoc. simpl. assumption.
  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], as [], as [], as [].
    destruct ( _ wfΣ) as [].
    unfold zipp in . simpl in .
    constructor.
    constructor.
    - destruct u as [na ty bo ra], v as [na' ty' bo' ra']. simpl in ×.
      unfold def_sig at 2. simpl.
      destruct fk.
      + intros. erewrite (abstract_env_ext_irr _ _ wfΣ); eauto.
       rewrite app_context_assoc in ; eauto.
      + intros. erewrite (abstract_env_ext_irr _ _ wfΣ); eauto.
       rewrite app_context_assoc in ; eauto.

    - eapply All2_impl. 1: exact .
      simpl. intros [? ? ? ?] [? ? ? ?] hh.
      simpl in ×.
      rewrite map_app in hh. simpl in hh.
      rewrite !app_assoc in hh. simpl in hh.
      assumption.
    Unshelve. all: eauto.
  Qed.
  Next Obligation.
    apply h''; clear h''.
    destruct H as [H]; inversion H; constructor.
    rewrite map_app, app_assoc; simpl; assumption.
  Qed.
  Next Obligation.
    apply h''; clear h''.
    destruct H as [H]; inversion H; constructor.
    destruct fk; cbn -[app_context].
    all: rewrite app_context_assoc; apply ; eauto.
  Qed.

  Equations isws_cumul_pb_Fix (fk : fix_kind) (Γ : context)
    (mfix : mfixpoint term) (idx : ) (π : stack)
    (h : wtp Γ (mFix fk mfix idx) π)
    (mfix' : mfixpoint term) (idx' : ) (π' : stack)
    (h' : wtp Γ (mFix fk mfix' idx') π')
    (hx : conv_stack_ctx Γ π π')
    (ei : idx = idx')
    (aux : Aux Term Γ (mFix fk mfix idx) π (mFix fk mfix' idx') π' h')
    : ConversionResult ( ( u v
          ( Σ (wfΣ : abstract_env_ext_rel X Σ), Σ ;;; Γ ,,, stack_context π u.(dtype) = v.(dtype)) ×
          ( Σ (wfΣ : abstract_env_ext_rel X Σ), Σ ;;; Γ ,,, stack_context π ,,, fix_context mfix u.(dbody) = v.(dbody)) ×
          (u.(rarg) = v.(rarg)) × eq_binder_annot u.(dname) v.(dname)
      ) mfix mfix' ) :=

      isws_cumul_pb_Fix fk Γ mfix idx π h mfix' idx' π' h' hx ei aux
    with
      isws_cumul_pb_fix_types fk Γ idx
        [] mfix π _
        [] mfix' π' _
        hx _ (expand aux)
    := {
    | Success
      with
        isws_cumul_pb_fix_bodies fk Γ idx
          [] mfix π _
          [] mfix' π' _
          hx _ _ (expand aux)
      := {
      | Success := yes ;
      | Error e h'' := no e
      } ;
    | Error e h'' := no e
    }.

  Next Obligation.
    destruct as [], as [].
    constructor.
    rewrite fix_context_fix_context_alt.
    pose proof (All2_mix ) as .
    eapply All2_impl. 1: exact .
    intros [? ? ? ?] [? ? ? ?] ?. simpl in ×.
    intuition eauto.
  Qed.
  Next Obligation.
    apply h''; clear h''.
    destruct H as [H]; constructor.
    apply (All2_impl H).
    rewrite fix_context_fix_context_alt. intuition.
  Qed.
  Next Obligation.
    apply h''; clear h''.
    destruct H as [H]; constructor; apply (All2_impl H).
    intuition.
  Qed.

  Lemma invert_type_mkApps_tProd Σ (wfΣ : abstract_env_ext_rel X Σ) Γ na A b args T :
    Σ;;; Γ mkApps (tProd na A b) args : T args = [].
  Proof using Type.
    intros typ.
    destruct ( _ wfΣ).
    apply PCUICValidity.inversion_mkApps in typ as (?&[typ_prod typ_args]).
    apply inversion_Prod in typ_prod as (?&?&?&?&?); [|easy].
    eapply PCUICSpine.typing_spine_strengthen in typ_args; eauto.
    2:{ eapply PCUICArities.isType_Sort. 2:pcuic.
        eapply wf_universe_product; now eapply typing_wf_universe. }
    clear -typ_args.
    depelim typ_args.
    - easy.
    - now apply ws_cumul_pb_Sort_Prod_inv in w.
  Qed.


  Lemma welltyped_zipc_tProd_appstack_nil Σ (wfΣ : abstract_env_ext_rel X Σ) {Γ na A B l ρ} :
    welltyped Σ Γ (zipc (tProd na A B) (appstack l ρ)) l = [].
  Proof using Type.
    pose proof ( _ wfΣ) as [].
    intros wh.
    rewrite zipc_appstack in wh.
    zip fold in wh.
    apply welltyped_context in wh; [|easy].
    cbn in wh.
    destruct l as [|? ? _] using List.rev_ind; [easy|].
    rewrite mkApps_app in wh.
    cbn in wh. destruct wh as (?&typ); auto.
    change (tApp ?h ?a) with (mkApps h [a]) in typ.
    rewrite mkApps_app in typ.
    now apply invert_type_mkApps_tProd in typ.
  Qed.


  Lemma reduced_case_discriminee_whne Σ (wfΣ : abstract_env_ext_rel X Σ) Γ π ci p c brs h :
    eqb_term (reduce_term
                RedFlags.default
                _ X (Γ,,, stack_context π) c h) c = true
    isred_full Γ (tCase ci p c brs) π
    whne RedFlags.default Σ (Γ,,, stack_context π) c.
  Proof using Type.
    intros eq ir. pose proof (heΣ _ wfΣ) as [[]].
    pose proof ( _ wfΣ).
    destruct ir as (_&[wh]); eauto.
    eapply eqb_term_upto_univ_impl with (p := wf_universeb Σ) (q := closedu) in eq; tea.
    2-3: intros; apply iff_reflect; eapply (abstract_env_compare_universe_correct _ wfΣ Conv) ; now eapply wf_universe_iff.
    2:{ intros. rewrite wf_universeb_instance_forall in ×.
      apply wf_universe_instance_iff in .
      apply wf_universe_instance_iff in .
      eapply (abstract_env_compare_global_instance_correct X wfΣ); eauto.
        intros. apply ; now eapply wf_universe_iff. }
    - epose proof (reduce_term_complete _ _ _ _ _ _) as [wh'].
      eapply whnf_eq_term in eq; [|exact wh'].
      rewrite zipp_as_mkApps in wh.
      depelim wh; solve_discr.
      apply whne_mkApps_inv in w as [|(?&?&?&?&?&?&?&?&?)]; [|easy|easy].
      depelim w; cbn in *; try easy; solve_discr.
      apply whnf_whne_nodelta_upgrade in eq; auto using sq.
    - pose proof (reduce_term_sound RedFlags.default X_type X (Γ,,, stack_context π) c h) as Hreduce.
      specialize_Σ wfΣ. pose proof (h _ wfΣ) as [C hc]. sq.
      apply closed_red_red in Hreduce. eapply PCUICSR.subject_reduction in hc; eauto.
      Opaque reduce_term.
      eapply typing_wf_universes in hc as [? ?]%andb_and; eauto.
    - clear eq. specialize_Σ wfΣ. sq. destruct h as [? h].
      eapply typing_wf_universes in h as [h h']%andb_and; eauto.
    Unshelve. all:eauto.
  Qed.


  Lemma welltyped_zipp_inv Σ Γ t π :
    wf Σ welltyped Σ Γ (zipp t π) welltyped Σ Γ t.
  Proof using Type.
    induction π; cbn; auto.
    unfold zipp.
    destruct decompose_stack.
    intros ? [s' Hs].
    eapply PCUICValidity.inversion_mkApps in Hs as [? []].
    now x.
  Qed.


  Lemma welltyped_zipc_inv Σ Γ t π : wf Σ welltyped Σ Γ (zipc t π) welltyped Σ (Γ,,, stack_context π) t.
  Proof.
    intros ? Ht. apply welltyped_zipc_zipp in Ht; eauto.
    apply welltyped_zipp_inv in Ht; eauto.
  Defined.


  Lemma welltyped_wf Σ Γ t : wf Σ welltyped Σ Γ t wf_universes Σ t.
  Proof using Type.
    intros ? [? Ht]. apply typing_wf_universes in Ht; eauto.
    cbn in Ht. rtoProp; intuition.
  Qed.


  Lemma inv_reduced_discriminees_case Σ (wfΣ : abstract_env_ext_rel X Σ) leq Γ π π' ci ci' p p' c c' brs brs' h h' :
    conv_stack_ctx Γ π π'
    true = eqb_term (reduce_term
                       RedFlags.default
                       _ X (Γ,,, stack_context π) c h) c
    true = eqb_term (reduce_term
                       RedFlags.default
                       _ X (Γ,,, stack_context π') c' h') c'
    welltyped Σ Γ (zipc (tCase ci p c brs) π)
    welltyped Σ Γ (zipc (tCase ci' p' c' brs') π')
    isred_full Γ (tCase ci p c brs) π
    isred_full Γ (tCase ci' p' c' brs') π'
    conv_cum
      leq Σ (Γ,,, stack_context π)
      (zipp (tCase ci p c brs) π)
      (zipp (tCase ci' p' c' brs') π')
     ci = ci',
     ws_cumul_pb_predicate Σ (Γ,,, stack_context π) p p',
     Σ;;; Γ,,, stack_context π c = c',
     ws_cumul_pb_brs Σ (Γ,,, stack_context π) p brs brs' &
     ws_cumul_pb_terms Σ (Γ,,, stack_context π) (decompose_stack π).1 (decompose_stack π').1].
  Proof using Type.
    intros [] c_is_red%eq_sym %eq_sym wtc wtc' cc; eauto.
    eapply reduced_case_discriminee_whne in c_is_red as ; eauto.
    eapply reduced_case_discriminee_whne in as ; eauto.
    destruct ( _ wfΣ) as [], as [], as [].
    rewrite !zipp_as_mkApps in cc.
    eapply whne_conv_context in .
    2:{ symmetry in . eapply ws_cumul_ctx_pb_forget in . exact . }
    apply conv_cum_mkApps_inv in cc as [(ws_cumul_pb_Case&conv_args)]; eauto using whnf_mkApps.
    red in .
    eapply welltyped_zipc_zipp, welltyped_zipp_inv in wtc; eauto.
    eapply welltyped_zipc_zipp, welltyped_zipp_inv in wtc'; eauto.
    destruct wtc. eapply inversion_Case in as [mdecl [idecl [isdecl [indices [[] ?]]]]]; tea.
    destruct wtc'. eapply inversion_Case in as [mdecl' [idecl' [isdecl' [indices' [[] ?]]]]] ; tea; eauto.
    eapply conv_cum_tCase_inv in ws_cumul_pb_Case; eauto.
    destruct ws_cumul_pb_Case as [[ ? ? ?]].
    split; split; auto.
  Qed.


  Lemma reduced_proj_body_whne Σ (wfΣ : abstract_env_ext_rel X Σ) Γ π p c h :
    true = eqb_term (reduce_term
                RedFlags.default
                _ X (Γ,,, stack_context π) c h) c
    isred_full Γ (tProj p c) π
    whne RedFlags.default Σ (Γ,,, stack_context π) c.
  Proof using Type.
    intros eq%eq_sym ir.
    destruct ir as (_&[wh]); eauto.
    pose proof ( _ wfΣ).
    eapply eqb_term_upto_univ_impl in eq; tea.
    2-3: intros; apply iff_reflect; eapply (abstract_env_compare_universe_correct _ wfΣ Conv) ; now eapply wf_universe_iff.
    2:{ intros. rewrite wf_universeb_instance_forall in ×.
        apply wf_universe_instance_iff in .
        apply wf_universe_instance_iff in .
        eapply (abstract_env_compare_global_instance_correct X wfΣ); eauto.
        intros. apply ; now eapply wf_universe_iff. }
    - epose proof (reduce_term_complete _ _ _ _ _ _) as [wh'].
      eapply whnf_eq_term in eq; [|exact wh'].
      rewrite zipp_as_mkApps in wh.
      depelim wh; solve_discr.
      apply whne_mkApps_inv in w as [|(?&?&?&?&?&?&?&?&?)]; [|easy|easy].
      depelim w; cbn in *; try easy; solve_discr.
      apply whnf_whne_nodelta_upgrade in eq; auto using sq.
    - pose proof (reduce_term_sound RedFlags.default X_type X (Γ,,, stack_context π) c h) as Hreduce.
      specialize_Σ wfΣ. pose proof (h _ wfΣ) as [C hc]. sq.
      apply closed_red_red in Hreduce. eapply PCUICSR.subject_reduction in hc; eauto.
      Opaque reduce_term.
      eapply typing_wf_universes in hc as [? ?]%andb_and; eauto.
    - clear eq. specialize_Σ wfΣ. sq. destruct h as [? h].
    eapply typing_wf_universes in h as [h h']%andb_and; eauto.
    Unshelve. all:eauto.
  Qed.


  Lemma inv_reduced_body_proj Σ (wfΣ : abstract_env_ext_rel X Σ) leq Γ π π' p p' c c' h h' :
    conv_stack_ctx Γ π π'
    true = eqb_term (reduce_term
                       RedFlags.default
                       _ X (Γ,,, stack_context π) c h) c
    true = eqb_term (reduce_term
                       RedFlags.default
                      _ X (Γ,,, stack_context π') c' h') c'
    isred_full Γ (tProj p c) π
    isred_full Γ (tProj p' c') π'
    conv_cum leq Σ (Γ,,, stack_context π) (zipp (tProj p c) π) (zipp (tProj p' c') π')
    p = p' ×
     Σ;;; Γ,,, stack_context π c = c' ×
     ws_cumul_pb_terms Σ (Γ,,, stack_context π) (decompose_stack π).1 (decompose_stack π').1.
  Proof using Type.
    intros [] c_is_red cc; eauto.
    eapply reduced_proj_body_whne in c_is_red as ; eauto.
    eapply reduced_proj_body_whne in as ; eauto.
    destruct ( _ wfΣ) as [], as [], as [].
    rewrite !zipp_as_mkApps in cc.
    eapply whne_conv_context in .
    2:{ symmetry in . eapply ws_cumul_ctx_pb_forget in . exact . }
    apply conv_cum_mkApps_inv in cc as [(conv_proj&conv_args)]; eauto using whnf_mkApps.
    eapply conv_cum_tProj_inv in conv_proj; eauto.
    destruct conv_proj as [(&?)].
    constructor; auto.
  Qed.


  Lemma conv_cum_red_conv_inv Σ (wfΣ : abstract_env_ext_rel X Σ) leq Γ Γ' t1 t2 t1' t2' :
    ws_cumul_ctx_pb Conv Σ Γ Γ'
    red Σ Γ
    red Σ Γ'
    sq_ws_cumul_pb leq Σ Γ
    sq_ws_cumul_pb leq Σ Γ .
  Proof using Type.
    intros. destruct ( _ wfΣ) as [].
    eapply conv_cum_red_conv_inv; eauto.
    all:eapply into_closed_red; tea.
    × fvs.
    × destruct H; fvs.
    × fvs.
    × destruct H. rewrite (All2_fold_length ). now eapply ws_cumul_pb_is_open_term_right.
  Qed.


  Lemma inv_stuck_fixes Σ (wfΣ : abstract_env_ext_rel X Σ) leq Γ mfix idx π mfix' idx' π' h h' :
    conv_stack_ctx Γ π π'
    None = unfold_one_fix Γ mfix idx π h
    None = unfold_one_fix Γ mfix' idx' π' h'
    conv_cum leq Σ (Γ,,, stack_context π) (zipp (tFix mfix idx) π) (zipp (tFix mfix' idx') π')
     idx = idx',
      ( d d'
             rarg d = rarg d' × eq_binder_annot d.(dname) d'.(dname) ×
             Σ;;; Γ,,, stack_context π dtype d = dtype d' ×
             Σ;;; Γ,,, stack_context π,,, fix_context mfix dbody d = dbody d')
          mfix mfix' &
     ws_cumul_pb_terms Σ (Γ,,, stack_context π) (decompose_stack π).1 (decompose_stack π').1].
  Proof using Type.
    intros [?] cc; eauto.
    rewrite !zipp_as_mkApps in cc; eauto.
    apply unfold_one_fix_None in .
    destruct as [(?&?&?)]; eauto.
    apply unfold_one_fix_None in .
    destruct as [(?&?&?)]; eauto.
    destruct ( _ wfΣ).
    eapply conv_cum_red_conv_inv in cc.
    2: eassumption.
    2: exact .
    2: eapply red_mkApps; [reflexivity|exact a].
    2: apply red_mkApps; [reflexivity|exact ].
    apply conv_cum_mkApps_inv in cc as [(ws_cumul_pb_Fix&conv_args)]; auto.
    2:{ eapply whnf_conv_context; eauto.
        symmetry in . now eapply ws_cumul_ctx_pb_forget in . }
    apply conv_cum_tFix_inv in ws_cumul_pb_Fix as [(&?)]; auto.
    sq; split; auto.
    × eapply All2_impl; tea; cbn. intros ? ? []. repeat split; auto.
    × eapply ws_cumul_pb_terms_red_conv; eauto.
      all:eapply into_red_terms; tea.
      1,3:fvs.
      + specialize_Σ wfΣ. eapply welltyped_zipc_zipp in h; auto.
        destruct h as [s h].
        rewrite zipp_as_mkApps in h.
        eapply subject_is_open_term in h.
        rewrite on_free_vars_mkApps in h. now apply andb_true_iff in h.
      + specialize_Σ wfΣ. eapply welltyped_zipc_zipp in h'; auto.
        destruct h' as [s h'].
        rewrite zipp_as_mkApps in h'.
        eapply subject_is_open_term in h'.
        rewrite on_free_vars_mkApps in h'. now apply andb_true_iff in h'.
  Qed.


  Lemma inv_stuck_cofixes Σ (wfΣ : abstract_env_ext_rel X Σ) leq Γ mfix idx π mfix' idx' π' :
    conv_stack_ctx Γ π π'
    conv_cum leq Σ (Γ,,, stack_context π) (zipp (tCoFix mfix idx) π) (zipp (tCoFix mfix' idx') π')
    idx = idx' ×
      ( d d'
             rarg d = rarg d' × eq_binder_annot d.(dname) d'.(dname) ×
             Σ;;; Γ,,, stack_context π dtype d = dtype d' ×
             Σ;;; Γ,,, stack_context π,,, fix_context mfix dbody d = dbody d')
          mfix mfix' ×
     ws_cumul_pb_terms Σ (Γ,,, stack_context π) (decompose_stack π).1 (decompose_stack π').1.
  Proof using Type.
    intros [?] cc; eauto. specialize_Σ wfΣ.
    rewrite !zipp_as_mkApps in cc.
    destruct ( _ wfΣ).
    apply conv_cum_mkApps_inv in cc as [(ws_cumul_pb_CoFix&conv_args)]; auto.
    apply conv_cum_tCoFix_inv in ws_cumul_pb_CoFix as [(&?)]; auto.
    constructor; split; [|split]; auto.
    eapply All2_impl; tea. intros ? ? []. repeat split; auto.
  Qed.


  Equations (noeqns) isconv_predicate_params_aux
            (Γ : context)
            (ci1 : case_info)
            (p1 : predicate term) (c1 : term) (brs1 : list (branch term))
            (π1 : stack)
            (h1 : wtp Γ (tCase ) π1)
            (ci2 : case_info)
            (p2 : predicate term) (c2 : term) (brs2 : list (branch term))
            (π2 : stack) (h2 : wtp Γ (tCase ) π2)
            (hx : conv_stack_ctx Γ π1 π2)
            (aux : Aux Term Γ (tCase ) π1 (tCase ) π2 )
            (pre1 pre2 post1 post2 : list term)
            (eq1 : .(pparams) = )
            (eq2 : .(pparams) = ) :
    ConversionResult ( Σ (wfΣ : abstract_env_ext_rel X Σ), ws_cumul_pb_terms Σ (Γ,,, stack_context π1) ) :=
    isconv_predicate_params_aux
      Γ π1 π2
      hx aux [] [] yes;
    
    isconv_predicate_params_aux
      Γ π1 π2
      hx aux ( :: ) ( :: )
      with isconv_red_raw
           Conv
            (Case_pred
                 
                 (pred_hole_params .(puinst) .(pcontext) .(preturn))
                  :: π1)
            (Case_pred
                 
                 (pred_hole_params .(puinst) .(pcontext) .(preturn))
                  :: π2) aux := {
      
      | Error ce not_conv_termno ce;

      | Success conv_tm
          with isconv_predicate_params_aux
               Γ π1 π2 hx aux
               ( []) ( []) _ _ := {
        
        | Error ce not_conv_restno ce;
        
        | Success conv_restyes
        }
      };

    isconv_predicate_params_aux
      Γ π1 π2 hx aux
       eq no (CasePredParamsUnequalLength
                                            (Γ,,, stack_context π1)
                                            (Γ,,, stack_context π2) ).
  Next Obligation.
    destruct (abstract_env_ext_exists X) as [[Σ wfΣ]];
    specialize_Σ wfΣ.
    destruct H as [H].
    depelim H.
  Qed.
  Next Obligation.
    destruct (abstract_env_ext_exists X) as [[Σ wfΣ]];
    specialize_Σ wfΣ.
    destruct H as [H].
    depelim H.
  Qed.
  Next Obligation.
    destruct ; auto.
  Qed.
  Next Obligation.
    destruct ; auto.
  Qed.
  Next Obligation.
    apply R_positionR. all: simpl.
    1: destruct ; cbn in *; subst; reflexivity.
    rewrite stack_position_cons.
    rewrite app_nil_r.
    eapply positionR_poscat.
    constructor.
  Qed.
  Next Obligation.
    rewrite app_assoc; auto.
  Qed.
  Next Obligation.
    rewrite app_assoc; auto.
  Qed.
  Next Obligation.
    specialize_Σ wfΣ.
    destruct conv_tm, conv_rest.
    unfold zipp in X; simpl in ×.
    constructor; constructor; auto.
  Qed.
  Next Obligation.
    contradiction not_conv_rest. intros.
    specialize_Σ wfΣ.
    destruct H as [H]; depelim H.
    constructor; auto.
  Qed.
  Next Obligation.
    contradiction not_conv_term. intros Σ wfΣ.
    specialize_Σ wfΣ.
    destruct H as [H]; depelim H.
    constructor; auto.
  Qed.

  Lemma case_conv_preds_inv Σ (wfΣ : abstract_env_ext_rel X Σ) {Γ ci p c brs brs' π}
  (h : wtp Γ (tCase ci p c brs) π)
  (p' : predicate term) (c' : term)
  (π' : stack) (h' : wtp Γ (tCase ci p' c' brs') π')
  (hx : conv_stack_ctx Γ π π')
  (hp : ws_cumul_pb_terms Σ (Γ,,, stack_context π) (pparams p) (pparams p') ) :
   mdecl idecl,
     declared_inductive Σ ci mdecl idecl,
      forallb (wf_universeb Σ) (map Universe.make (puinst p)),
      forallb (wf_universeb Σ) (map Universe.make (puinst p')),
       #|pparams p| = ind_npars mdecl,
       #|pparams p'| = ind_npars mdecl,
       eq_context_gen eq eq p.(pcontext) p'.(pcontext),
       test_context_k ( k : on_free_vars (closedP k ( _ : true)))
         #|pparams p| p.(pcontext) &
       test_context_k ( k : on_free_vars (closedP k ( _ : true)))
         #|pparams p'| p'.(pcontext)] .
  Proof using Type.
    destruct ( _ wfΣ). specialize_Σ wfΣ.
    destruct hx as [hx].
    destruct hp as [hp].
    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' _]].
    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 (clp : test_context_k ( k : on_free_vars (closedP k ( _ : true)))
      #|pparams p| p.(pcontext)).
    { rewrite test_context_k_closed_on_free_vars_ctx.
      destruct hcase.
      eapply PCUICConfluence.eq_context_upto_names_on_free_vars.
      2:symmetry; exact conv_pctx.
      rewrite closedn_ctx_on_free_vars.
      eapply PCUICClosed.closedn_ctx_upwards.
      { eapply (closed_ind_predicate_context); tea.
        eapply declared_minductive_closed; tea. exact decli'. }
      rewrite (wf_predicate_length_pars wf_pred).
      now rewrite (PCUICGlobalEnv.declared_minductive_ind_npars decli).
    }
    rewrite test_context_k_closed_on_free_vars_ctx.
     mdecl, idecl.
    destruct hcase. destruct hcase'.
    split; tea.
    - eapply Forall_forallb; try eapply consistent_instance_wf_universe; eauto.
      intros; apply wf_universe_iff; eauto.
    - eapply Forall_forallb; try eapply consistent_instance_wf_universe; eauto.
      intros; apply wf_universe_iff; eauto.
    - eapply (wf_predicate_length_pars wf_pred).
    - eapply (wf_predicate_length_pars wf_pred0).
    - eapply alpha_eq_context_gen. etransitivity; tea.
      now symmetry.
    - now rewrite test_context_k_closed_on_free_vars_ctx.
    - rewrite test_context_k_closed_on_free_vars_ctx.
      eapply PCUICConfluence.eq_context_upto_names_on_free_vars.
      2:symmetry; exact conv_pctx0.
      rewrite closedn_ctx_on_free_vars.
      relativize #|pparams p'|.
      { eapply (closed_ind_predicate_context); tea.
        eapply declared_minductive_closed; tea. exact decli'. }
      rewrite (wf_predicate_length_pars wf_pred0).
      now rewrite (PCUICGlobalEnv.declared_minductive_ind_npars decli).
  Qed.


  Definition forallb2_proper A B (R R' : A B bool) l l':
    ( a b, R a b = R' a b)
     R l l' =
     R' l l'.
  Proof using Type.
    intro e. revert l'.
    induction l; destruct l'; eauto.
    cbn; intros. rewrite e.
    apply eq_true_iff_eq. split; intros.
     all: apply andb_and; now apply andb_and in H.
  Qed.


  Definition isconv_predicate_params
            (Γ : context)
            (ci1 : case_info)
            (p1 : predicate term) (c1 : term) (brs1 : list (branch term))
            (π1 : stack)
            (h1 : wtp Γ (tCase ) π1)
            (ci2 : case_info)
            (p2 : predicate term) (c2 : term) (brs2 : list (branch term))
            (π2 : stack) (h2 : wtp Γ (tCase ) π2)
            (hx : conv_stack_ctx Γ π1 π2)
            (aux : Aux Term Γ (tCase ) π1 (tCase ) π2 ) :=
    isconv_predicate_params_aux Γ π1 π2 hx aux [] []
                                .(pparams) .(pparams) eq_refl eq_refl.

  Equations (noeqns) isconv_predicate
            (Γ : context)
            (ci1 : case_info)
            (p1 : predicate term) (c1 : term) (brs1 : list (branch term))
            (π1 : stack)
            (h1 : wtp Γ (tCase ) π1)
            (ci2 : case_info)
            (p2 : predicate term) (c2 : term) (brs2 : list (branch term))
            (π2 : stack) (h2 : wtp Γ (tCase ) π2)
            (hx : conv_stack_ctx Γ π1 π2)
            (eqci : = )
            (aux : Aux Term Γ (tCase ) π1 (tCase ) π2 )
    : ConversionResult ( Σ (wfΣ : abstract_env_ext_rel X Σ), ws_cumul_pb_predicate Σ (Γ,,, stack_context π1) ) :=

    isconv_predicate Γ π1 π2 hx eqci aux
      with isconv_predicate_params
           Γ π1 π2 hx aux := {

      | Error ce not_conv_paramsno ce;

      | Success conv_params
        with inspect (eqb_universe_instance_gen (abstract_env_eq X) .(puinst) .(puinst)) := {

        | exist false not_eq_instsno (CasePredUnequalUniverseInstances
                                            (Γ,,, stack_context π1)
                                            (Γ,,, stack_context π2) );

        | exist true eq_insts
            with isconv_red_raw
                 Conv .(preturn)
                      (Case_pred (pred_hole_return .(pparams) .(puinst) .(pcontext))
                                  :: π1)
                      .(preturn)
                      (Case_pred (pred_hole_return .(pparams) .(puinst) .(pcontext))
                                  :: π2)
                      aux := {

            | Error ce not_conv_retno ce;

            | Success conv_retyes
          }
        }
      }.
  Next Obligation.
    destruct ; cbn in *; subst; auto.
  Qed.
  Next Obligation.
    destruct ; cbn in *; subst; auto.
  Qed.
  Next Obligation.
    apply R_positionR. all: simpl.
    1: destruct ; cbn in *; subst; reflexivity.
    rewrite stack_position_cons.
    rewrite app_nil_r.
    eapply positionR_poscat.
    constructor.
  Qed.
  Next Obligation.
    rename H into wfΣ.
    destruct ( _ wfΣ).
    eapply eq_sym, eqb_universe_instance_spec in eq_insts; eauto.
    - destruct (case_conv_preds_inv _ wfΣ _ _ _ hx (conv_params _ wfΣ)) as []; tea.
      specialize_Σ wfΣ. destruct hx as [hx].
    destruct conv_params as [conv_params].
    constructor.
    unfold app_context; rewrite !app_assoc.
    destruct as [mdecl [idecl []]].
    etransitivity.
    × inv_on_free_vars. eapply (inst_case_ws_cumul_ctx_pb d e ); tea. fvs.
    × eapply ws_cumul_ctx_pb_app_same. 2:eapply hx.
      rewrite on_free_vars_ctx_app.
      apply andb_true_iff. split; auto.
      1:now eapply ws_cumul_ctx_pb_closed_left in hx.
      eapply on_free_vars_ctx_inst_case_context; trea.
      fvs.
     - destruct (case_conv_preds_inv _ wfΣ _ _ _ hx (conv_params Σ wfΣ)) as []; tea.
       destruct as [mdecl [idecl []]]. eauto.
     - destruct (case_conv_preds_inv _ wfΣ _ _ _ hx (conv_params Σ wfΣ)) as []; tea.
       destruct as [mdecl [idecl []]]. eauto.
  Qed.
  Next Obligation.
    unfold zipp in conv_ret; simpl in conv_ret.
    destruct (case_conv_preds_inv _ wfΣ _ _ _ hx (conv_params Σ wfΣ)) as []; tea.
    eapply eq_sym, eqb_universe_instance_spec in eq_insts; eauto.
    - specialize_Σ wfΣ. destruct hx as [hx]. destruct conv_params as [conv_params].
    destruct conv_ret as [h].
    split. split; auto.
    2:rewrite app_context_assoc in h; auto.
    now destruct as [mdecl [idecl []]].
    - now destruct as [mdecl [idecl []]].
    - now destruct as [mdecl [idecl []]].
  Qed.
  Next Obligation.
    unfold zipp in not_conv_ret; simpl in not_conv_ret.
    contradiction not_conv_ret.
    rewrite app_context_assoc. intros Σ wfΣ. specialize_Σ wfΣ.
    destruct H as [[]]; constructor; auto.
  Qed.
  Next Obligation.
    destruct (abstract_env_ext_exists X) as [[Σ wfΣ]].
    destruct ( _ wfΣ).
    zip fold in .
    eapply welltyped_context in as (?&); eauto.
    eapply inversion_Case in as (?&?&?&?&[]&?); auto.
    zip fold in .
    clear aux.
    eapply welltyped_context in as (?&); eauto.
    apply inversion_Case in as (?&?&?&?&[]&?); auto.
    apply consistent_instance_ext_wf in cons.
    apply consistent_instance_ext_wf in .
    specialize_Σ wfΣ; destruct H as [[]].
    apply eqb_universe_instance_complete in r; eauto.
    unfold eqb_universe_instance in r.
    congruence.
  Qed.
  Next Obligation.
    contradiction not_conv_params. intros Σ wfΣ.
    specialize_Σ wfΣ.
    destruct H as [[]]; constructor; auto.
  Qed.

  Lemma conv_cum_red_inv Σ (wfΣ : abstract_env_ext_rel X Σ) leq Γ t1 t2 t1' t2' :
    red Σ Γ
    red Σ Γ
    sq_ws_cumul_pb leq Σ Γ
    sq_ws_cumul_pb leq Σ Γ .
  Proof using Type.
    intros. destruct ( _ wfΣ).
    destruct H. eapply conv_cum_red_inv; tea. 3:split; eauto.
    all:eapply into_closed_red; tea; fvs.
  Qed.



  Opaque reduce_stack.
  Equations(noeqns) _isconv_prog (Γ : context) (leq : conv_pb)
            (t1 : term) (π1 : stack) (h1 : wtp Γ π1)
            (t2 : term) (π2 : stack) (h2 : wtp Γ π2)
            (hx : conv_stack_ctx Γ π1 π2)
            (ir1 : isred_full Γ π1) (ir2 : isred_full Γ π2)
            (aux : Aux Term Γ π1 π2 )
    : ConversionResult (conv_term leq Γ π1 π2) :=

    _isconv_prog Γ leq π1 π2 hx aux with prog_viewc := {
    | prog_view_App _ _ _ _ := False_rect _ _;

    | prog_view_Const c u c' u' with eq_dec c c' := {
      | left with inspect (eqb_universe_instance_gen (abstract_env_eq X) u u') := {
        | @exist true with isconv_args_raw leq (tConst c u) π1 (tConst c' u') π2 aux := {
          | Success h := yes ;
          
          | Error e h with inspect (abstract_env_lookup X c) := {
            | @exist (Some (ConstantDecl {| cst_body := Some body |})) :=
              isconv_red leq (subst_instance u body) π1
                             (subst_instance u' body) π2 aux ;
            
            | @exist _ _ := no (NotFoundConstant c)
            }
          } ;
        
        | @exist false uneq_u := unfold_constants Γ leq c u π1 c' u' π2 _ hx aux
        } ;
      
      | right uneq_c := unfold_constants Γ leq c u π1 c' u' π2 _ hx aux
      } ;

    | prog_view_Lambda na na'
      with isconv_red_raw Conv (Lambda_ty na :: π1)
                                (Lambda_ty na' :: π2) aux := {
      | Success h with inspect (eqb_binder_annot na na') := {
        | exist true _ :=
          isconv_red leq
                      (Lambda_bd na :: π1)
                      (Lambda_bd na' :: π2) aux ;
        | exist false e :=
          no (
            LambdaNotConvertibleAnn
              (Γ ,,, stack_context π1) na
              (Γ ,,, stack_context π2) na'
          ) };
      | Error e h :=
        no (
          LambdaNotConvertibleTypes
            (Γ ,,, stack_context π1) na
            (Γ ,,, stack_context π2) na' e
        )
      } ;

    | prog_view_Prod na na'
      with isconv_red_raw Conv (Prod_l na :: π1) (Prod_l na' :: π2) aux := {
      | Success h with inspect (eqb_binder_annot na na') := {
        | exist true _ :=
          isconv_red leq
                    (Prod_r na :: π1)
                    (Prod_r na' :: π2) aux ;
        | exist false e :=
          no (
            ProdNotConvertibleAnn
              (Γ ,,, stack_context π1) na
              (Γ ,,, stack_context π2) na'
          ) };
      | Error e h :=
        no (
          ProdNotConvertibleDomains
            (Γ ,,, stack_context π1) na
            (Γ ,,, stack_context π2) na' e
        )
      } ;

    | prog_view_Case ci p c brs ci' p' c' brs'
      with inspect (reduce_term RedFlags.default _ X (Γ ,,, stack_context π1) c _) := {
      | @exist cred with inspect (eqb_term cred c) := {
        | @exist true with inspect (reduce_term RedFlags.default _ X (Γ ,,, stack_context π2) c' _) := {
          | @exist cred' with inspect (eqb_term cred' c') := {
            | @exist true with inspect (eqb ci ci') := {
              | @exist true
                  with isconv_predicate Γ ci p c brs π1 _ ci' p' c' brs' π2 _ _ _ aux := {
                | Success convp with isconv_red_raw Conv
                                  c (Case_discr ci p brs :: π1)
                                  c' (Case_discr ci' p' brs' :: π2) aux := {
                  | Success convdiscr with isconv_branches' Γ ci p c brs π1 _ ci' p' c' brs' π2 _ _ _ _ aux := {
                    | Success convbrs with isconv_args_raw leq (tCase ci p c brs) π1 (tCase ci' p' c' brs') π2 aux := {
                      | Success convargs := yes ;
                      | Error e h := no e
                      } ;
                    | Error e h := no e
                    } ;
                  | Error e h := no e
                  } ;
                | Error e h := no e
                } ;
              | @exist false :=
                no (
                  CaseOnDifferentInd
                    (Γ ,,, stack_context π1) ci p c brs
                    (Γ ,,, stack_context π2) ci' p' c' brs'
                )
              } ;
            | @exist false :=
              isconv_red leq
                (tCase ci p c brs) π1
                (tCase ci' p' cred' brs') π2
                aux
            }
          } ;
        | @exist false :=
          isconv_red leq
            (tCase ci p cred brs) π1
            (tCase ci' p' c' brs') π2
            aux
        }
      } ;

    | prog_view_Proj p c p' c' with inspect (reduce_term RedFlags.default _ X (Γ ,,, stack_context π1) c _) := {
      | @exist cred with inspect (eqb_term cred c) := {
        | @exist true with inspect (reduce_term RedFlags.default _ X (Γ ,,, stack_context π2) c' _) := {
          | @exist cred' with inspect (eqb_term cred' c') := {
            | @exist true with inspect (eqb p p') := {
              | @exist true with isconv_red_raw Conv c (Proj p :: π1) c' (Proj p' :: π2) aux := {
                | Success convdiscr := isconv_args leq (tProj p c) π1 (tProj p' c') π2 aux ;
                | Error e h := no e
                } ;
              | @exist false :=
                no (
                  DistinctStuckProj
                    (Γ ,,, stack_context π1) p c
                    (Γ ,,, stack_context π2) p' c'
                )
              } ;
            | @exist false :=
              isconv_red leq
                (tProj p c) π1
                (tProj p' cred') π2
                aux
          }
        } ;
        | @exist false :=
          isconv_red leq
            (tProj p cred) π1
            (tProj p' c') π2
            aux
      }
    } ;
    | prog_view_Fix mfix idx mfix' idx'
      with inspect (unfold_one_fix Γ mfix idx π1 _) := {
      | @exist (Some (fn, θ)) with inspect (decompose_stack θ) := {
        | @exist (l', θ')
          with inspect (reduce_stack RedFlags.nodelta _ X (Γ ,,, stack_context θ') fn (appstack l' []) _) := {
          | @exist (fn', ρ) :=
            isconv_prog leq fn' θ') (tFix mfix' idx') π2 aux
          }
        } ;
      | @exist None eee with inspect (unfold_one_fix Γ mfix' idx' π2 _) := {
        | @exist (Some (fn, θ))
          with inspect (decompose_stack θ) := {
          | @exist (l', θ')
            with inspect (reduce_stack RedFlags.nodelta _ X (Γ ,,, stack_context θ') fn (appstack l' []) _) := {
            | @exist (fn', ρ) :=
              isconv_prog leq (tFix mfix idx) π1 fn' θ') aux
            }
          } ;
        | @exist None with inspect (eqb idx idx') := {
          | @exist true with isws_cumul_pb_Fix IndFix Γ mfix idx π1 _ mfix' idx' π2 _ _ _ aux := {
            | Success convfix with isconv_args_raw leq (tFix mfix idx) π1 (tFix mfix' idx') π2 aux := {
              | Success convargs := yes ;
              | Error e h := no e
              } ;
            | Error e h := no e
            } ;
          | @exist false idx_uneq :=
            no (
              CannotUnfoldFix
                (Γ ,,, stack_context π1) mfix idx
                (Γ ,,, stack_context π2) mfix' idx'
            )
          }
        }
      } ;

    | prog_view_CoFix mfix idx mfix' idx'
      with inspect (eqb idx idx') := {
      | @exist true with isws_cumul_pb_Fix CoIndFix Γ mfix idx π1 _ mfix' idx' π2 _ _ _ aux := {
        | Success convfix with isconv_args_raw leq (tCoFix mfix idx) π1 (tCoFix mfix' idx') π2 aux := {
          | Success convargs := yes ;
          | Error e h := no e
          } ;
        | Error e h := no e
        } ;
      | @exist false idx_uneq :=
        no (
          DistinctCoFix
            (Γ ,,, stack_context π1) mfix idx
            (Γ ,,, stack_context π2) mfix' idx'
        )
      } ;

    | prog_view_other h :=
      isconv_fallback leq π1 π2 aux
    }.

  Next Obligation.
    destruct as [ _]. discriminate .
  Qed.

  Next Obligation.
    eapply R_stateR. all: try reflexivity.
    simpl. constructor.
  Qed.
  Next Obligation.
    rename H into wfΣ; destruct ( _ wfΣ). clear aux.
    specialize_Σ wfΣ.
    apply conv_cum_zipp; auto.
    constructor. eapply ws_cumul_pb_eq_le_gen.
    constructor. all:fvs.
    - destruct h. eapply welltyped_zipc_zipp in ; auto. fvs.
    - constructor. eapply eqb_universe_instance_spec; eauto.
      + eapply welltyped_zipc_tConst_inv in as (?&?&?); eauto;
        eapply Forall_forallb; try eapply consistent_instance_wf_universe; eauto.
        intros; apply wf_universe_iff; eauto.
      + eapply welltyped_zipc_tConst_inv in as (?&?&?); eauto;
        eapply Forall_forallb; try eapply consistent_instance_wf_universe; eauto.
        intros; apply wf_universe_iff; eauto.
  Qed.
  Next Obligation.
    pose (heΣ _ wfΣ). specialize_Σ wfΣ. sq.
    eapply red_welltyped ; [auto|..].
    - exact .
    - eapply red_zipc.
      eapply red_const. erewrite abstract_env_lookup_correct; eauto.
  Qed.
  Next Obligation.
    pose (heΣ _ wfΣ). clear aux. specialize_Σ wfΣ. sq.
    eapply red_welltyped ; [auto|..].
    - exact .
    - 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 ( _ wfΣ).
    specialize_Σ wfΣ.
    etransitivity.
    - eapply red_conv_cum_l ; try assumption.
      eapply closed_red_zipp. 1:eapply welltyped_zipc_zipp in ; fvs.
      eapply into_closed_red.
      × eapply red_const. erewrite abstract_env_lookup_correct; eauto.
      × eapply welltyped_zipc_zipp in ; fvs.
      × eapply welltyped_zipc_zipp in ; fvs.
    - etransitivity ; try eassumption.
      eapply red_conv_cum_r ; try assumption.
      eapply closed_red_zipp; auto.
      2:{ eapply into_closed_red; auto.
        × eapply red_const. erewrite abstract_env_lookup_correct; eauto.
        × eapply welltyped_zipc_zipp in ; fvs. }
      clear aux. eapply welltyped_zipc_zipp in ; eauto.
      destruct hx as [hx]. rewrite (All2_fold_length hx); fvs.
      Unshelve. all:eauto.
  Qed.
  Next Obligation.
    apply h; cbn; clear h. intros Σ wfΣ.
    destruct ( _ wfΣ).
    eapply conv_cum_red_inv.
    - eauto.
    - apply red_zipp.
      eapply red_const. erewrite abstract_env_lookup_correct; eauto.
    - apply red_zipp.
      eapply red_const. erewrite abstract_env_lookup_correct; eauto.
    - now eapply H.
  Qed.
  Next Obligation.
    apply h; clear h. intros Σ wfΣ.
    rewrite !zipp_as_mkApps in H.
    destruct ( _ wfΣ).
    eapply conv_cum_mkApps_inv in H as [(?&?)]; eauto.
    - apply whnf_mkApps.
      eapply whne_const.
      + erewrite abstract_env_lookup_correct; eauto.
      + eauto.
    - apply whnf_mkApps.
      eapply whne_const.
      + erewrite abstract_env_lookup_correct; eauto.
      + eauto.
  Qed.
  Next Obligation.
    destruct (abstract_env_ext_exists X) as [[Σ wfΣ]];
    eapply welltyped_zipc_tConst_inv in as (?&?&?); eauto.
    unfold declared_constant in ×.
    erewrite abstract_env_lookup_correct in d; eauto. congruence.
  Qed.
  Next Obligation.
  destruct (abstract_env_ext_exists X) as [[Σ wfΣ]];
  eapply welltyped_zipc_tConst_inv in as (?&?&?); eauto.
  unfold declared_constant in ×.
  erewrite abstract_env_lookup_correct in d; eauto. congruence.
Qed.
  Next Obligation.
    destruct (abstract_env_ext_exists X) as [[Σ wfΣ]];
    right; split; [easy|].
    unfold eqb_universe_instance.
    now rewrite uneq_u.
  Qed.

  Next Obligation.
    unshelve eapply R_positionR.
    - reflexivity.
    - simpl. rewrite app_nil_r, stack_position_cons. eapply positionR_poscat. constructor.
  Qed.
  Next Obligation.
    unshelve eapply R_positionR.
    - reflexivity.
    - simpl. rewrite app_nil_r, stack_position_cons. eapply positionR_poscat. constructor.
  Qed.
  Next Obligation.
    rename H into wfΣ; specialize_Σ wfΣ.
    destruct hx as [hx].
    destruct h as [h].
    constructor. constructor. 1: assumption.
    constructor.
    - symmetry in e. now apply eqb_binder_annot_spec.
    - assumption.
  Qed.
  Next Obligation.
    rename H into wfΣ; specialize_Σ wfΣ.
    destruct as [].
    destruct hx as [hx].
    apply isred_full_nobeta in ; [|easy].
    apply isred_full_nobeta in ; [|easy].
    cbn in ×.
    simpl_stacks.
    destruct ( _ wfΣ).
    symmetry in e; apply eqb_binder_annot_spec in e.
    now eapply conv_cum_Lambda.
  Qed.
  Next Obligation.
    apply h; clear h. intros Σ wfΣ; specialize_Σ wfΣ.
    destruct as [].
    destruct hx as [hx].
    apply isred_full_nobeta in ; [|easy].
    apply isred_full_nobeta in ; [|easy].
    cbn in ×.
    simpl_stacks.
    destruct ( _ wfΣ).
    symmetry in e; apply eqb_binder_annot_spec in e.
    apply Lambda_conv_cum_inv in H as (?&?&?); auto.
  Qed.
  Next Obligation.
    symmetry in .
    destruct (abstract_env_ext_exists X) as [[Σ wfΣ]];
    specialize_Σ wfΣ.
    destruct hx as [hx].
    apply isred_full_nobeta in ; [|easy].
    apply isred_full_nobeta in ; [|easy].
    cbn in ×.
    simpl_stacks.
    destruct ( _ wfΣ).
    apply Lambda_conv_cum_inv in H as (?&?&?); auto.
    eapply (ssrbool.elimF (eqb_annot_reflect _ _)) in ; auto.
  Qed.
  Next Obligation.
    apply h; clear h. intros Σ wfΣ. specialize_Σ wfΣ.
    destruct hx as [hx].
    apply isred_full_nobeta in ; [|easy].
    apply isred_full_nobeta in ; [|easy].
    cbn in ×.
    simpl_stacks.
    destruct ( _ wfΣ).
    apply Lambda_conv_cum_inv in H as (?&?&?); auto.
  Qed.

  Next Obligation.
    unshelve eapply R_positionR.
    - reflexivity.
    - simpl. rewrite app_nil_r, stack_position_cons. eapply positionR_poscat. constructor.
  Qed.
  Next Obligation.
    unshelve eapply R_positionR.
    - simpl. reflexivity.
    - simpl. rewrite app_nil_r, stack_position_cons. eapply positionR_poscat. constructor.
  Qed.
  Next Obligation.
    rename H into wfΣ; specialize_Σ wfΣ.
    destruct hx as [hx].
    destruct h as [h].
    constructor. constructor. 1: assumption.
    constructor.
    - symmetry in e.
      now apply eqb_binder_annot_spec.
    - assumption.
  Qed.
  Next Obligation.
    rename H into wfΣ; specialize_Σ wfΣ.
    destruct ( _ wfΣ) as [].
    destruct as [].
    destruct hx as [hx].
    cbn in ×.
    apply welltyped_zipc_zipp in ; auto.
    clear aux.
    eapply welltyped_zipc_zipp in ; eauto.
    rewrite !zipp_as_mkApps in ×.
    apply mkApps_Prod_nil in as ; auto.
    apply mkApps_Prod_nil in as ; auto.
    destruct h.
    symmetry in e.
    apply eqb_binder_annot_spec in e.
    split; eapply ws_cumul_pb_Prod; auto.
  Qed.
  Next Obligation.
    apply h; clear h.
    symmetry in e. apply eqb_binder_annot_spec in e.
    intros Σ wfΣ. specialize_Σ wfΣ.
    destruct ( _ wfΣ) as [], as [], hx as [hx].
    cbn in ×.
    apply welltyped_zipc_zipp in ; auto.
    clear aux.
    eapply welltyped_zipc_zipp in ; eauto.
    rewrite !zipp_as_mkApps in ×.
    apply mkApps_Prod_nil in ; auto.
    apply mkApps_Prod_nil in ; auto.
    rewrite , in H.
    apply Prod_conv_cum_inv in H as (?&_&?); auto.
  Qed.
  Next Obligation.
    destruct (abstract_env_ext_exists X) as [[Σ wfΣ]].
    specialize_Σ wfΣ.
    destruct ( _ wfΣ) as [].
    destruct hx as [hx].
    cbn in ×.
    apply welltyped_zipc_zipp in ; auto.
    clear aux.
    eapply welltyped_zipc_zipp in ; eauto.
    rewrite !zipp_as_mkApps in ×.
    apply mkApps_Prod_nil in ; auto.
    apply mkApps_Prod_nil in ; auto.
    rewrite , in H.
    apply Prod_conv_cum_inv in H as (?&?&?); auto.
    eapply (ssrbool.elimF (eqb_annot_reflect _ _)); tea.
    now unfold eqb_binder_annot.
  Qed.
  Next Obligation.
    apply h; clear h. intros Σ wfΣ. specialize_Σ wfΣ.
    destruct ( _ wfΣ) as [], hx as [hx].
    cbn in ×.
    apply welltyped_zipc_zipp in ; auto.
    clear aux.
    eapply welltyped_zipc_zipp in ; eauto.
    rewrite !zipp_as_mkApps in ×.
    apply mkApps_Prod_nil in ; auto.
    apply mkApps_Prod_nil in ; auto.
    rewrite , in H.
    apply Prod_conv_cum_inv in H as (?&?&_); auto.
  Qed.
  Next Obligation.
    rename H into wfΣ; specialize_Σ wfΣ.
    destruct ( _ wfΣ) as [].
    zip fold in . apply welltyped_context in ; auto. simpl in .
    destruct as [T ].
    apply inversion_Case in as hh ; auto.
    destruct hh as [mdecl [idecl [isdecl [indices [[] cum]]]]].
    eexists. eassumption.
  Qed.
  Next Obligation.
    rename H into wfΣ; specialize_Σ wfΣ.
    destruct ( _ wfΣ) as [].
    clear aux.
    zip fold in . eapply welltyped_context in ; eauto. simpl in .
    destruct as [T ].
    apply inversion_Case in as hh ; auto.
    destruct hh as [mdecl [idecl [isdecl [indices [[] cum]]]]].
    eexists. eassumption.
  Qed.
  Next Obligation.
    now apply eqb_eq.
  Qed.
  Next Obligation.
    eapply R_positionR. all: simpl.
    1: reflexivity.
    rewrite app_nil_r, stack_position_cons.
    eapply positionR_poscat. constructor.
  Qed.
  Next Obligation.
    now apply eqb_eq.
  Qed.
  Next Obligation.
    unshelve eapply R_stateR.
    all: try reflexivity.
    simpl. constructor.
  Qed.
  Next Obligation.
    pose proof hx as hx'.
    rename H into wfΣ; specialize_Σ wfΣ.
    pose proof (heΣ _ wfΣ) as [].
    apply conv_cum_zipp; auto.
    destruct convp as [], convbrs as [], convargs as [].
    destruct convdiscr as [cdiscr]. cbn in cdiscr.
    unfold zipp in , . simpl in , .
    sq.
    apply ws_cumul_pb_eq_le_gen.
    change (eq_dec_to_bool ci ci') with (eqb ci ci') in .
    destruct (eqb_specT ci ci'). 2: discriminate.
    subst. eapply ws_cumul_pb_Case. all: tas.
    × clear aux . eapply welltyped_zipc_zipp in ; eauto.
      eapply welltyped_is_open_term in .
      rewrite zipp_as_mkApps in .
      rewrite on_free_vars_mkApps in .
      now apply andb_true_iff in as [].
    × clear aux . eapply welltyped_zipc_zipp in ; eauto.
      eapply welltyped_is_open_term in .
      rewrite zipp_as_mkApps in .
      rewrite on_free_vars_mkApps in .
      unfold is_open_case. rewrite (All2_fold_length hx').
      now apply andb_true_iff in as [].
  Qed.
  Next Obligation.
    apply h; clear h. intros.
    eapply inv_reduced_discriminees_case in H as [[]]; eauto.
  Qed.
  Next Obligation.
    apply h; cbn; clear h. intros.
    eapply inv_reduced_discriminees_case in H as [[]]; eauto.
  Qed.
  Next Obligation.
    apply h; cbn; clear h. intros.
    eapply inv_reduced_discriminees_case in H as [[]]; eauto.
    constructor; auto.
  Qed.
  Next Obligation.
    apply h; cbn; clear h. intros.
    eapply inv_reduced_discriminees_case in H as [[]]; eauto.
  Qed.
  Next Obligation.
    destruct (abstract_env_ext_exists X) as [[Σ wfΣ]];
    specialize_Σ wfΣ.
    eapply inv_reduced_discriminees_case in H as [[]]; eauto.
    now destruct (eqb_spec ci ci).
  Qed.
  Next Obligation.
    pose proof (heΣ _ wfΣ) as []. pose proof as .
    specialize_Σ wfΣ.
    match goal with
      | |- context [ reduce_term ?f ?Σ ? ?Γ ?t ?h ] ⇒
        pose proof (reduce_term_sound f Σ Γ t h) as [hr]
    end; eauto.
    eapply red_welltyped ; [auto|..].
    - exact .
    - eapply red_zipc.
      eapply red_case_c; auto. eapply hr.
  Qed.
  Next Obligation.
    destruct (abstract_env_ext_exists X) as [[Σ wfΣ]];
    specialize_Σ wfΣ.
    match goal with
    | |- context [ reduce_term ?f _ ?X ?Γ c' ?h ] ⇒
      destruct (reduce_stack_Req f _ X _ wfΣ Γ c' [] h) as [e' | hr]
    end.
    1:{
      exfalso. Transparent reduce_term.
      unfold reduce_term in .
      rewrite e' in . cbn in .
      epose proof (eqb_term_upto_univ_refl Σ _ _ _ _ 0 c' _ _).
      rewrite H in .
      - discriminate.
      - intros. apply iff_reflect. eapply abstract_env_compare_universe_correct; eauto.
      - intros. rewrite wf_universeb_instance_forall in ×.
        apply wf_universe_instance_iff in .
        apply wf_universe_instance_iff in .
        eapply abstract_env_compare_global_instance_correct; eauto.
      - pose proof as Hc. specialize_Σ wfΣ. pose proof ( _ wfΣ); sq.
        apply welltyped_zipc_inv in Hc; eauto.
        apply welltyped_wf in Hc; eauto.
        cbn in Hc. rtoProp; intuition.
    }
    dependent destruction hr.
    2:{
      exfalso.
      destruct y'. simpl in . inversion . subst.
      unfold reduce_term in .
      rewrite in .
      cbn in .
      epose proof (eqb_term_upto_univ_refl Σ _ _ _ _ 0 c' _ _).
      rewrite in .
      - discriminate.
      - intros. apply iff_reflect. eapply abstract_env_compare_universe_correct; eauto.
      - intros. rewrite wf_universeb_instance_forall in ×.
        apply wf_universe_instance_iff in .
        apply wf_universe_instance_iff in .
        eapply abstract_env_compare_global_instance_correct; eauto.
      - pose proof as Hc. specialize_Σ wfΣ. pose proof ( _ wfΣ); sq.
        apply welltyped_zipc_inv in Hc; eauto.
        apply welltyped_wf in Hc; eauto.
        cbn in Hc. rtoProp; intuition.
    }
    unshelve eapply R_cored2.
    all: try reflexivity.
    simpl. intros. eapply cored_zipc. eapply cored_case.
    erewrite (abstract_env_ext_irr _ _ wfΣ); eauto.
    Unshelve. all: eauto. all: intros; eapply abstract_env_compare_universe_correct; eauto; reflexivity.
  Qed.

  Next Obligation.
    rename H into wfΣ; pose proof ( _ wfΣ) as w.
    pose proof hx as hx'; specialize_Σ wfΣ. destruct w.
    destruct hx' as [hx'].
    match type of h with
    | context [ reduce_term ?f ?Σ ? ?Γ c' ?h ] ⇒
      pose proof (reduce_term_sound f Σ Γ c' h) as hr
    end.
    destruct (hr _ wfΣ) as [hr'].
    etransitivity.
    - eassumption.
    - eapply conv_cum_conv_ctx; tea.
      eapply red_conv_cum_r ; try assumption.
      eapply into_closed_red.
      × eapply red_zipp.
        eapply red_case_c. eapply hr'.
      × fvs.
      × clear aux h hr'.
        clear hr. eapply welltyped_zipc_zipp in ; fvs.
        Unshelve. all:eauto.
  Qed.
  Next Obligation.
    apply h; clear h. intros Σ wfΣ.
    pose proof ( _ wfΣ) as []. pose proof hx as hx'.
    specialize_Σ wfΣ.
    destruct hx'.
    epose proof (reduce_term_sound _ _ _ _ _ _) as [r]; eauto.
    eapply conv_cum_red_conv_inv.
    all: tea.
    1: reflexivity.
    eapply red_zipp.
    apply red_case_c.
    exact r.
  Qed.

  Next Obligation.
    pose proof (heΣ _ wfΣ) as []. pose proof as .
    clear aux . specialize_Σ wfΣ.
    match goal with
      | |- context [ reduce_term ?f ?Σ ? ?Γ ?t ?h ] ⇒
        pose proof (reduce_term_sound f Σ Γ t h) as [hr]
    end; eauto.
    sq.
    eapply red_welltyped ; [auto|..].
    - exact .
    - eapply red_zipc.
      apply red_case_c, hr.
  Qed.
  Next Obligation.
    destruct (abstract_env_ext_exists X) as [[Σ wfΣ]].
    match goal with
    | |- context [ reduce_term ?f _ ?X ?Γ c ?h ] ⇒
      destruct (reduce_stack_Req f _ X _ wfΣ Γ c [] h) as [e' | hr]
    end.
    1:{
      exfalso.
      unfold reduce_term in .
      rewrite e' in . cbn in .
      epose proof (eqb_term_upto_univ_refl Σ _ _ _ _ 0 c _ _).
      rewrite H in .
      - discriminate.
      - intros. apply iff_reflect. eapply abstract_env_compare_universe_correct; eauto.
      - intros. rewrite wf_universeb_instance_forall in ×.
        apply wf_universe_instance_iff in .
        apply wf_universe_instance_iff in .
        eapply abstract_env_compare_global_instance_correct; eauto.
      - pose proof as Hc. specialize_Σ wfΣ. pose proof ( _ wfΣ); sq.
        apply welltyped_zipc_inv in Hc; eauto.
        apply welltyped_wf in Hc; eauto.
        cbn in Hc. rtoProp; intuition.
    }
    dependent destruction hr.
    2:{
      exfalso.
      destruct y'. simpl in . inversion . subst.
      unfold reduce_term in .
      rewrite in .
      cbn in .
      epose proof (eqb_term_upto_univ_refl Σ _ _ _ _ 0 c _ _).
      rewrite in .
      - discriminate.
      - intros. apply iff_reflect. eapply abstract_env_compare_universe_correct; eauto.
      - intros. rewrite wf_universeb_instance_forall in ×.
        apply wf_universe_instance_iff in .
        apply wf_universe_instance_iff in .
        eapply abstract_env_compare_global_instance_correct; eauto.
      - pose proof as Hc. specialize_Σ wfΣ. pose proof ( _ wfΣ); sq.
        apply welltyped_zipc_inv in Hc; eauto.
        apply welltyped_wf in Hc; eauto.
        cbn in Hc. rtoProp; intuition.
    }
    unshelve eapply R_cored.
    simpl. intros; eapply cored_zipc. eapply cored_case.
    erewrite (abstract_env_ext_irr _ _ wfΣ); eauto.
    Unshelve. all: eauto. all: intros; eapply abstract_env_compare_universe_correct; eauto; reflexivity.
  Qed.
  Next Obligation.
    rename H into wfΣ; specialize_Σ wfΣ.
    destruct ( _ wfΣ) as [].
    destruct hx as [hx].
    match type of h with
    | context [ reduce_term ?f ?Σ ? ?Γ c ?h ] ⇒
      pose proof (reduce_term_sound f Σ Γ c h) as hr
    end.
    destruct (hr _ wfΣ) as [hr'].
    etransitivity.
    - eapply red_conv_cum_l ; try assumption.
      eapply into_closed_red.
      × eapply red_zipp.
        eapply red_case_c, hr'.
      × fvs.
      × clear h hr' hr; eapply welltyped_zipc_zipp in ; fvs.
    - assumption.
    Unshelve. all:eauto.
  Qed.
  Next Obligation.
    apply h; clear h. intros Σ wfΣ.
    pose proof ( _ wfΣ) as [].
    destruct (hx _ wfΣ).
    epose proof (reduce_term_sound _ _ _ _ _ _) as [r]; eauto.
    eapply conv_cum_red_inv.
    1: eauto.
    2: reflexivity.
    - apply red_zipp, red_case_c, r.
    - destruct (H _ wfΣ) as []. sq; eauto.
  Qed.

  Next Obligation.
    rename H into wfΣ. destruct ( _ wfΣ) as [].
    zip fold in . eapply welltyped_context in ; eauto. simpl in .
    destruct as [T ].
    apply inversion_Proj in as hh. 2: auto.
    destruct hh as [? [? [? [? [? [? [? [? ?]]]]]]]].
    eexists. eassumption.
  Qed.
  Next Obligation.
    rename H into wfΣ. destruct ( _ wfΣ) as [].
    zip fold in . eapply welltyped_context in as ; eauto. simpl in .
    destruct as [T ].
    apply inversion_Proj in as hh. 2: auto.
    destruct hh as [? [? [? [? [? [? [? [? ?]]]]]]]].
    eexists. eassumption.
  Qed.
  Next Obligation.
    eapply R_aux_positionR. all: simpl.
    - reflexivity.
    - rewrite app_nil_r, stack_position_cons. apply positionR_poscat. constructor.
  Qed.
  Next Obligation.
    unshelve eapply R_stateR.
    all: try reflexivity.
    simpl. constructor.
  Qed.
  Next Obligation.
    rename H into wfΣ. destruct (heΣ _ wfΣ) as [].
    specialize_Σ wfΣ.
    destruct convdiscr as [].
    change (true = eqb p p') in .
    destruct (eqb_spec p p'). 2: discriminate. subst.
    apply conv_cum_zipp; auto.
    clear aux. eapply conv_conv_cum_l.
    now eapply ws_cumul_pb_Proj_c.
  Qed.
  Next Obligation.
    apply h; cbn; clear h. intros Σ wfΣ.
    eapply inv_reduced_body_proj in H; eauto.
    destruct H as [(&?&?)].
    constructor; auto.
  Qed.
  Next Obligation.
    apply h; cbn; clear h. intros Σ wfΣ.
    eapply inv_reduced_body_proj in H; eauto.
    destruct H as [(&?&?)].
    constructor; auto.
  Qed.
  Next Obligation.
    destruct (abstract_env_ext_exists X) as [[Σ wfΣ]].
    eapply inv_reduced_body_proj in H; eauto.
    destruct H as [(&?&?)].
    now rewrite eqb_refl in .
  Qed.
  Next Obligation.
    pose proof (heΣ _ wfΣ) as [].
    match goal with
    | |- context [ reduce_term ?f ?Σ ? ?Γ ?t ?h ] ⇒
      pose proof (reduce_term_sound f Σ Γ t h) as [hr]
    end; eauto.
    eapply red_welltyped ; [auto|..].
    - exact ( _ wfΣ).
    - eapply red_zipc.
      eapply red_proj_c, hr.
  Qed.
  Next Obligation.
    destruct (abstract_env_ext_exists X) as [[Σ wfΣ]].
    match goal with
    | |- context [ reduce_term ?f _ ?X ?Γ c' ?h ] ⇒
      destruct (reduce_stack_Req f _ X _ wfΣ Γ c' [] h) as [e' | hr]
    end.
    1:{
      exfalso.
      unfold reduce_term in .
      rewrite e' in . cbn in .
      epose proof (eqb_term_upto_univ_refl Σ _ _ _ _ 0 c' _ _).
      rewrite H in .
      - discriminate.
      - intros. apply iff_reflect. eapply abstract_env_compare_universe_correct; eauto.
      - intros. rewrite wf_universeb_instance_forall in ×.
        apply wf_universe_instance_iff in .
        apply wf_universe_instance_iff in .
        eapply abstract_env_compare_global_instance_correct; eauto.
      - pose proof as Hc. specialize_Σ wfΣ. pose proof ( _ wfΣ); sq.
        apply welltyped_zipc_inv in Hc; eauto.
        apply welltyped_wf in Hc; eauto.
    }
    dependent destruction hr.
    2:{
      exfalso.
      destruct y'. simpl in . inversion . subst.
      unfold reduce_term in .
      rewrite in .
      cbn in .
      epose proof (eqb_term_upto_univ_refl Σ _ _ _ _ 0 c' _ _).
      rewrite in .
      - discriminate.
      - intros. apply iff_reflect. eapply abstract_env_compare_universe_correct; eauto.
      - intros. rewrite wf_universeb_instance_forall in ×.
        apply wf_universe_instance_iff in .
        apply wf_universe_instance_iff in .
        eapply abstract_env_compare_global_instance_correct; eauto.
      - pose proof as Hc. specialize_Σ wfΣ. pose proof ( _ wfΣ); sq.
        apply welltyped_zipc_inv in Hc; eauto.
        apply welltyped_wf in Hc; eauto.
    }
    unshelve eapply R_cored2.
    all: try reflexivity.
    simpl. intros; eapply cored_zipc. eapply cored_proj.
    erewrite (abstract_env_ext_irr _ _ wfΣ); eassumption.
    Unshelve. all: eauto. all: intros; eapply abstract_env_compare_universe_correct; eauto; reflexivity.
  Qed.
  Next Obligation.
    rename H into wfΣ. specialize_Σ wfΣ.
    pose proof ( _ wfΣ) as w. destruct w.
    destruct hx as [hx].
    match type of h with
    | context [ reduce_term ?f ?Σ ? ?Γ c' ?h ] ⇒
      pose proof (reduce_term_sound f Σ Γ c' h) as hr
    end.
    destruct (hr _ wfΣ) as [hr'].
    etransitivity.
    - eassumption.
    - eapply conv_cum_conv_ctx; tea.
      eapply red_conv_cum_r ; try assumption.
      eapply into_closed_red.
      × eapply red_zipp.
        eapply red_proj_c, hr'.
      × fvs.
      × clear hr hr' h aux. eapply welltyped_zipc_zipp in ; fvs.
      Unshelve. all:eauto.
  Qed.
  Next Obligation.
    apply h; cbn; clear h. intros Σ wfΣ.
    pose proof ( _ wfΣ) as w. destruct w.
    specialize_Σ wfΣ.
    destruct hx as [hx].
    match type of with
    | context [ reduce_term ?f ?Σ ? ?Γ c' ?h ] ⇒
      pose proof (reduce_term_sound f Σ Γ c' h) as hr
    end.
    destruct (hr _ wfΣ) as [hr'].
    etransitivity; [eassumption|].
    eapply conv_cum_conv_ctx; eauto.
    eapply red_conv_cum_l ; try assumption.
    eapply into_closed_red.
    × eapply red_zipp.
      eapply red_proj_c, hr'.
    × fvs.
    × clear aux hr hr'. eapply welltyped_zipc_zipp in ; fvs.
    Unshelve. all:eauto.
  Qed.
  Next Obligation.
    pose proof (heΣ _ wfΣ) as [].
    match goal with
      | |- context [ reduce_term ?f _ ?X ?Γ ?t ?h ] ⇒
        pose proof (reduce_term_sound f _ X Γ t h) as [hr]
    end; eauto.
    sq.
    eapply red_welltyped ; [auto|..].
    - exact ( _ wfΣ).
    - eapply red_zipc.
      eapply red_proj_c, hr.
  Qed.
  Next Obligation.
    destruct (abstract_env_ext_exists X) as [[Σ wfΣ]].
    match goal with
    | |- context [ reduce_term ?f _ ?X ?Γ c ?h ] ⇒
      destruct (reduce_stack_Req f _ X _ wfΣ Γ c [] h) as [e' | hr]
    end.
    1:{
      exfalso.
      unfold reduce_term in .
      rewrite e' in . cbn in .
      epose proof (eqb_term_upto_univ_refl Σ _ _ _ _ 0 c _ _).
      rewrite H in .
      - discriminate.
      - intros. apply iff_reflect. eapply abstract_env_compare_universe_correct; eauto.
      - intros. rewrite wf_universeb_instance_forall in ×.
        apply wf_universe_instance_iff in .
        apply wf_universe_instance_iff in .
        eapply abstract_env_compare_global_instance_correct; eauto.
      - pose proof as Hc. specialize_Σ wfΣ. pose proof ( _ wfΣ); sq.
        apply welltyped_zipc_inv in Hc; eauto.
        apply welltyped_wf in Hc; eauto.
    }
    dependent destruction hr.
    2:{
      exfalso.
      destruct y'. simpl in . inversion . subst.
      unfold reduce_term in .
      rewrite in .
      cbn in .
      epose proof (eqb_term_upto_univ_refl Σ _ _ _ _ 0 c _ _).
      rewrite in .
      - discriminate.
      - intros. apply iff_reflect. eapply abstract_env_compare_universe_correct; eauto.
      - intros. rewrite wf_universeb_instance_forall in ×.
        apply wf_universe_instance_iff in .
        apply wf_universe_instance_iff in .
        eapply abstract_env_compare_global_instance_correct; eauto.
      - pose proof as Hc. specialize_Σ wfΣ. pose proof ( _ wfΣ); sq.
        apply welltyped_zipc_inv in Hc; eauto.
        apply welltyped_wf in Hc; eauto.
    }
    unshelve eapply R_cored.
    simpl. intros; eapply cored_zipc. eapply cored_proj.
    erewrite (abstract_env_ext_irr _ _ wfΣ); eassumption.
    Unshelve. all: eauto. all: intros; eapply abstract_env_compare_universe_correct; eauto; reflexivity.
  Qed.
  Next Obligation.
    rename H into wfΣ. specialize_Σ wfΣ.
    destruct ( _ wfΣ) as [].
    destruct hx as [hx].
    match type of h with
    | context [ reduce_term ?f ?Σ ? ?Γ c ?h ] ⇒
      pose proof (reduce_term_sound f Σ Γ c h) as hr
    end.
    destruct (hr _ wfΣ) as [hr'].
    etransitivity.
    - eapply red_conv_cum_l ; try assumption.
      eapply into_closed_red.
      × eapply red_zipp.
        eapply red_proj_c, hr'.
      × fvs.
      × clear aux hr hr' h. eapply welltyped_zipc_zipp in ; fvs.
    - assumption.
    Unshelve. all:eauto.
  Qed.
  Next Obligation.
    apply h; cbn; clear h. intros Σ wfΣ.
    destruct ( _ wfΣ) as []. specialize_Σ wfΣ.
    destruct hx as [hx].
    match type of with
    | context [ reduce_term ?f ?Σ ? ?Γ c ?h ] ⇒
      pose proof (reduce_term_sound f Σ Γ c h) as hr
    end.
    destruct (hr _ wfΣ) as [hr'].
    etransitivity.
    - eapply red_conv_cum_r ; try assumption.
      eapply into_closed_red.
      × eapply red_zipp.
        eapply red_proj_c, hr'.
      × fvs.
      × clear hr hr' H . eapply welltyped_zipc_zipp in ; fvs.
    - assumption.
    Unshelve. all:eauto.
  Qed.

  Next Obligation.
    pose proof ( _ wfΣ) as .
    cbn. rewrite zipc_appstack. cbn.
    eapply unfold_one_fix_red_zipp in as r; eauto.
    sq.
    apply unfold_one_fix_decompose in as d.
    rewrite in d. simpl in d.
    unfold zipp in r.
    rewrite in r.
    case_eq (decompose_stack π1). intros ρ1 .
    rewrite in r.
    rewrite in d. simpl in d. subst.
    eapply welltyped_zipc_zipp in as ; eauto.
    pose proof (decompose_stack_eq _ _ _ ). subst.
    unfold zipp in . rewrite in .
    pose proof (red_welltyped _ r) as hh.
    rewrite stack_context_appstack in hh.
    assumption.
  Qed.
  Next Obligation.
    pose proof (heΣ _ wfΣ).
    eapply unfold_one_fix_red in as ; eauto.
    eapply unfold_one_fix_decompose in as .
    reduce_stack_facts Σ wfΣ.
    simpl_stacks.
    sq.
    eapply red_welltyped.
    1: eauto.
    1: exact ( _ wfΣ).
    etransitivity.
    2: { apply red_zipc.
         rewrite stack_context_decompose.
         exact r. }
    simpl_stacks.
    eassumption.
  Qed.
  Next Obligation.
    destruct (abstract_env_ext_exists X) as [[Σ wfΣ]];
    pose proof (heΣ _ wfΣ) as heΣ.
    specialize_Σ wf.
    eapply unfold_one_fix_cored in as ; eauto.
    eapply unfold_one_fix_decompose in as .
    match type of with
    | _ = reduce_stack ?f _ ?X ?Γ ?t ?π ?h
      destruct (reduce_stack_sound f _ X _ wfΣ Γ t π h) as []
    end.
    rewrite in .
    eapply R_cored. simpl. intros.
    erewrite (abstract_env_ext_irr _ _ wfΣ); eauto.
    eapply red_cored_cored ; try eassumption.
    eapply clrel_rel in .
    apply red_context_zip in . cbn in .
    rewrite zipc_stack_cat.
    pose proof (decompose_stack_eq _ _ _ (eq_sym )). subst.
    rewrite zipc_appstack in . cbn in .
    rewrite zipc_appstack.
    assumption.
    Unshelve. all: eauto.
  Qed.
  Next Obligation.
    apply unfold_one_fix_decompose in as .
    reduce_stack_facts Σ H.
    now simpl_stacks.
  Qed.
  Next Obligation.
    destruct (abstract_env_ext_exists X) as [[Σ wfΣ]].
    simpl_reduce_stack Σ wfΣ.
    specialize (isr eq_refl) as (?&_).
    split; [easy|]. intros.
    cbn in ×. erewrite (abstract_env_ext_irr _ _ wfΣ); eauto.
    now simpl_stacks.
    Unshelve. all:eauto.
  Qed.

  Lemma wt_zip_mkapps Σ (wfΣ:abstract_env_ext_rel X Σ) Γ f π : welltyped Σ Γ (zipc f π) is_open_term (Γ ,,, stack_context π) (mkApps f (decompose_stack π).1).
  Proof using Type.
    pose (heΣ _ wfΣ).
    sq.
    intros. apply welltyped_zipc_zipp in H; auto.
    rewrite zipp_as_mkApps in H. fvs.
  Qed.


  Next Obligation.
    eapply unfold_one_fix_red_zipp in as ; eauto.
    eapply unfold_one_fix_decompose in as .
    reduce_stack_facts Σ H.
    simpl_reduce_stack Σ H.
    destruct ( _ H), as [].
    eapply conv_cum_trans; auto.
    eapply red_conv_cum_l.
    etransitivity. 2:eauto.
    eapply into_closed_red; tea; [fvs|].
    eapply (f_equal stack_context) in .
    rewrite !stack_context_decompose in . rewrite .
    now eapply wt_zip_mkapps.
    Unshelve. all:eauto.
  Qed.
  Next Obligation.
    apply h; clear h. intros Σ wfΣ.
    eapply unfold_one_fix_red_zipp in as ; eauto.
    apply unfold_one_fix_decompose in as .
    reduce_stack_facts Σ wfΣ.
    simpl_reduce_stack Σ wfΣ.
    destruct ( _ wfΣ), as [].
    eapply conv_cum_red_inv.
    × eauto.
    × exact r.
    × auto.
    × specialize_Σ wfΣ. etransitivity; eauto.
      split. eapply ws_cumul_pb_eq_le_gen. symmetry.
      eapply red_ws_cumul_pb.
      eapply into_closed_red.
      + eapply .
      + fvs.
      + eapply (f_equal stack_context) in .
        rewrite !stack_context_decompose in . rewrite .
        now eapply wt_zip_mkapps.
  Qed.
  Next Obligation.
    pose proof (heΣ _ wfΣ).
    eapply unfold_one_fix_red_zipp in as r; eauto.
    sq.
    apply unfold_one_fix_decompose in as d.
    clear aux .
    eapply welltyped_zipc_zipp in ; eauto.
    cbn in ×.
    simpl_stacks.
    eapply red_welltyped; eauto.
  Qed.
  Next Obligation.
    pose proof ( _ wfΣ) as .
    eapply unfold_one_fix_red in as ; eauto.
    sq.
    apply unfold_one_fix_decompose in as .
    match type of with
    | _ = reduce_stack ?f _ ?X ?Γ ?t ?π ?h
      destruct (reduce_stack_sound f _ X _ wfΣ Γ t π h) as [] ;
      pose proof (reduce_stack_decompose RedFlags.nodelta _ X _ _ _ h) as ;
      pose proof (reduce_stack_context f _ X Γ t π h) as
    end.
    rewrite in . cbn in . rewrite zipc_appstack in . cbn in .
    rewrite in . cbn in . rewrite decompose_stack_appstack in .
    cbn in .
    rewrite in . cbn in . rewrite stack_context_appstack in .
    cbn in .
    case_eq (decompose_stack ρ). intros l ξ e.
    rewrite e in . cbn in . subst.
    pose proof (red_welltyped _ ( _ wfΣ) ) as hh.
    apply clrel_rel, red_context_zip in .
    pose proof (decompose_stack_eq _ _ _ (eq_sym )). subst.
    rewrite zipc_appstack in hh. cbn in .
    pose proof (red_welltyped _ hh ) as hh'.
    rewrite zipc_stack_cat. assumption.
  Qed.
  Next Obligation.
    destruct (abstract_env_ext_exists X) as [[Σ wfΣ]];
    pose proof (heΣ _ wfΣ) as heΣ.
    eapply unfold_one_fix_cored in as ; eauto.
    apply unfold_one_fix_decompose in as .
    match type of with
    | _ = reduce_stack ?f _ ?X ?Γ ?t ?π ?h
      destruct (reduce_stack_sound f _ X _ wfΣ Γ t π h) as []
    end.
    rewrite in .
    eapply R_cored2. all: try reflexivity. simpl. intros.
    erewrite (abstract_env_ext_irr _ _ wfΣ); eauto.
    eapply red_cored_cored ; try eassumption.
    cbn in .
    rewrite zipc_stack_cat.
    pose proof (decompose_stack_eq _ _ _ (eq_sym )). subst.
    rewrite zipc_appstack in . cbn in .
    rewrite zipc_appstack.
    do 2 zip fold. eapply red_context_zip, .
    Unshelve. eauto.
  Qed.
  Next Obligation.
    apply unfold_one_fix_decompose in as .
    match type of with
    | _ = reduce_stack ?f ?Σ ? ?Γ ?t ?π ?h
      pose proof (reduce_stack_decompose RedFlags.nodelta _ _ _ _ h) as
    end.
    rewrite in . cbn in .
     rewrite decompose_stack_appstack in .
    cbn in .
    rewrite in . simpl in .
    case_eq (decompose_stack π2). intros ρ2 .
    rewrite in . simpl in . subst.
    case_eq (decompose_stack ρ). intros l ξ e'.
    rewrite e' in . simpl in . subst.
    apply decompose_stack_eq in e' as ?. subst.
    rewrite stack_cat_appstack.
    rewrite stack_context_appstack.
    apply decompose_stack_eq in as ?. subst.
    clear .
    rewrite stack_context_appstack in hx.
    eauto.
  Qed.
  Next Obligation.
    destruct (abstract_env_ext_exists X) as [[Σ wfΣ]].
    simpl_reduce_stack Σ wfΣ.
    specialize (isr eq_refl) as (?&_).
    split; [easy|]. intros. erewrite (abstract_env_ext_irr _ _ wfΣ); eauto.
    simpl_stacks.
    eauto.
  Unshelve. all: eauto.
  Qed.
  Next Obligation.
    eapply unfold_one_fix_red_zipp in as ; eauto.
    apply unfold_one_fix_decompose in as .
    reduce_stack_facts Σ H.
    simpl_reduce_stack Σ H.
    destruct as []. specialize_Σ H.
    destruct ( _ H), hx.
    eapply conv_cum_red_conv.
    1,4: eauto.
    × eapply closed_red_refl; [fvs|].
      now eapply wt_zip_mkapps.
    × etransitivity; eauto.
      eapply into_closed_red.
      + eapply .
      + fvs.
      + eapply (f_equal stack_context) in .
        rewrite !stack_context_decompose in . rewrite .
        now eapply wt_zip_mkapps.
  Qed.
  Next Obligation.
    apply h; clear h. intros Σ wfΣ.
    eapply unfold_one_fix_red_zipp in as ; eauto.
    apply unfold_one_fix_decompose in as .
    reduce_stack_facts Σ wfΣ.
    simpl_reduce_stack Σ wfΣ.
    destruct as [].
    destruct ( Σ wfΣ), (hx Σ wfΣ).
    specialize (H Σ wfΣ).
    eapply conv_cum_red_conv_inv.
    1,2,5: eauto.
    × eapply closed_red_refl. 1:fvs.
      now eapply wt_zip_mkapps.
    × etransitivity; eauto. sq.
      eapply r.
  Qed.
  Next Obligation.
    change (true = eqb idx idx') in .
    destruct (eqb_spec idx idx'). 2: discriminate.
    assumption.
  Qed.
  Next Obligation.
    eapply R_stateR.
    all: simpl.
    all: try reflexivity.
    constructor.
  Qed.
  Next Obligation.
    pose proof ( _ H) as []. specialize_Σ H.
    apply conv_cum_zipp; auto.
    destruct convfix as [].
    eapply conv_conv_cum_l.
    change (true = eqb idx idx') in .
    destruct (eqb_specT idx idx'). 2: discriminate.
    subst.
    eapply ws_cumul_pb_Fix; eauto.
    - clear aux eee. eapply welltyped_zipc_zipp in ; fvs.
    - eapply All2_impl; eauto. intros.
      split; try eapply ; eauto.
      split; try eapply ; eauto.
  Qed.
  Next Obligation.
    apply h; clear h. intros.
    eapply inv_stuck_fixes in H as [[]]; eauto.
  Qed.
  Next Obligation.
    apply h; clear h.
    destruct (abstract_env_ext_exists X) as [[Σ wfΣ]].
    eapply inv_stuck_fixes in H as [[]]; eauto.
    constructor; auto.
    eapply All2_impl; eauto. cbn; intros.
    destruct as [Xr [Xe [Xd Xb]]].
    cbn; intros. repeat split; intros; eauto.
    - erewrite (abstract_env_ext_irr _ _ wfΣ); eauto.
    - erewrite (abstract_env_ext_irr _ _ wfΣ); eauto.
    Unshelve. all: eauto.
  Qed.
  Next Obligation.
    destruct (abstract_env_ext_exists X) as [[Σ wfΣ]].
    eapply inv_stuck_fixes in H as [[]]; eauto.
    now rewrite eqb_refl in idx_uneq.
  Qed.

  Next Obligation.
    change (true = eqb idx idx') in .
    destruct (eqb_spec idx idx'). 2: discriminate.
    assumption.
  Qed.
  Next Obligation.
    eapply R_stateR.
    all: simpl.
    all: try reflexivity.
    constructor.
  Qed.
  Next Obligation.
    rename H into wfΣ. pose proof ( _ wfΣ) as [].
    apply conv_cum_zipp; auto.
    destruct convfix as [].
    eapply conv_conv_cum_l.
    change (true = eqb idx idx') in .
    destruct (eqb_specT idx idx'). 2: discriminate.
    subst.
    eapply ws_cumul_pb_CoFix; eauto.
    - clear aux . eapply welltyped_zipc_zipp in ; fvs.
    - eapply All2_impl; eauto. now cbn; intros.
  Qed.
  Next Obligation.
    apply h; clear h. intros.
    eapply inv_stuck_cofixes in H as [(&?&?)]; eauto.
  Qed.
  Next Obligation.
    apply h; clear h.
    destruct (abstract_env_ext_exists X) as [[Σ wfΣ]].
    eapply inv_stuck_cofixes in H as [(&?&?)]; eauto.
    constructor; auto.
    eapply All2_impl; eauto; cbn; intros.
    destruct as [Xr [Xe [Xd Xb]]].
    repeat split; intros; eauto.
    - erewrite (abstract_env_ext_irr _ _ wfΣ); eauto.
    - erewrite (abstract_env_ext_irr _ _ wfΣ); eauto.
    Unshelve. all: eauto.
  Qed.
  Next Obligation.
    destruct (abstract_env_ext_exists X) as [[Σ wfΣ]].
    eapply inv_stuck_cofixes in H as [(&?&?)]; eauto.
    rewrite eqb_refl in idx_uneq.
    congruence.
  Qed.

  Next Obligation.
    unshelve eapply R_stateR.
    all: try reflexivity.
    simpl. constructor.
  Qed.

  Definition Aux' Γ t1 args1 l1 π1 t2 π2 h2 :=
     u1 u2 ca1 a1 ρ2
      (h1' : wtp Γ (App_r (mkApps ) :: appstack π1))
      (h2' : wtp Γ ρ2),
      let x :=
        mkpack Γ Reduction (App_r (mkApps ) :: (appstack π1)) ρ2
      in
      let y := mkpack Γ Args (mkApps ) (appstack π1) π2 in
      (S #|| + #|| = #|| + #||)%
      pzt x = pzt y
      positionR (` (pps1 x)) (` (pps1 y))
      Ret Reduction Γ (App_r (mkApps ) :: (appstack π1)) ρ2.

  Equations(noeqns) _isconv_args' (leq : conv_pb) (Γ : context)
            (t1 : term) (args1 : list term)
            (l1 : list term) (π1 : stack)
            (h1 : wtp Γ (mkApps ) (appstack π1))
            (hπ1 : isStackApp π1 = false)
            (t2 : term)
            (l2 : list term) (π2 : stack)
            (h2 : wtp Γ (appstack π2))
            (hπ2 : isStackApp π2 = false)
            (hx : conv_stack_ctx Γ π1 π2)
            (aux : Aux' Γ π1 (appstack π2) )
    : ConversionResult ( Σ (wfΣ : abstract_env_ext_rel X Σ), ws_cumul_pb_terms Σ (Γ,,, stack_context π1) ) by struct :=
    _isconv_args' leq Γ ( :: ) π1 hπ1 ( :: ) π2 hπ2 hx aux
    with aux (App_r :: (appstack π2)) _ _ _ _ Conv _ I I I := {
    | Success with _isconv_args' leq Γ ( []) π1 _ _ (tApp ) π2 _ _ _ (expand aux) := {
      | Success := yes ;
      | Error e herr :=
        no (
          StackTailError
            leq
            (Γ ,,, stack_context π1)
            (Γ ,,, stack_context π2) e
        )
      } ;
    | Error e herr :=
      no (
        StackHeadError
          leq
          (Γ ,,, stack_context π1)
          (Γ ,,, stack_context π2) e
      )
    } ;

    _isconv_args' leq Γ [] π1 hπ1 [] π2 hπ2 hx aux := yes ;

    _isconv_args' leq Γ π1 hπ1 π2 hπ2 hx aux :=
      no (
        StackMismatch
          (Γ ,,, stack_context π1)
          (Γ ,,, stack_context π2)
      ).
  Next Obligation.
    destruct (abstract_env_ext_exists X) as [[Σ wfΣ]].
    destruct (H _ wfΣ) as [H']; depelim H'.
  Qed.
  Next Obligation.
    destruct (abstract_env_ext_exists X) as [[Σ wfΣ]].
    destruct (H _ wfΣ) as [H']; depelim H'.
  Qed.
  Next Obligation.
    split. 1: reflexivity.
    rewrite !stack_position_cons.
    eapply positionR_poscat. constructor.
  Qed.
  Next Obligation.
    rewrite 2!stack_context_appstack.
    eauto.
  Qed.
  Next Obligation.
    rewrite mkApps_app. eauto.
  Qed.
  Next Obligation.
    rewrite app_length in h. cbn in h. .
  Qed.
  Next Obligation.
    rewrite app_length in h. cbn in h.
      simpl. split.
      + rewrite mkApps_app in H. assumption.
      + rewrite !stack_position_cons, !stack_position_appstack.
        rewrite !app_assoc. apply positionR_poscat.
        assert (h' : n m, positionR (repeat app_l n [app_r]) (repeat app_l m)).
        { clear. intro n. induction n ; intro m.
          - destruct m ; constructor.
          - destruct m.
            + constructor.
            + cbn. constructor. apply IHn.
        }
        simpl.
        rewrite repeat_snoc.
        apply (h' #|d| (S #||)).
  Defined.
  Next Obligation.
    specialize_Σ wfΣ.
    destruct ( _ wfΣ) as [].
    destruct as [].
    unfold zipp. simpl.
    unfold zipp in . simpl in .
    rewrite stack_context_appstack in .
    destruct as [].
    constructor; constructor; auto.
  Qed.
  Next Obligation.
    apply herr; clear herr. intros Σ wfΣ. specialize_Σ wfΣ.
    destruct H as [H]; depelim H.
    constructor; auto.
  Qed.
  Next Obligation.
    apply herr; cbn; clear herr. intros Σ wfΣ. specialize_Σ wfΣ.
    destruct H as [H]; depelim H.
    rewrite stack_context_appstack.
    constructor; auto.
  Qed.

  Equations(noeqns) _isconv_args (leq : conv_pb) (Γ : context)
           (t1 : term) (π1 : stack) (h1 : wtp Γ π1)
           (t2 : term) (π2 : stack) (h2 : wtp Γ π2)
           (hx : conv_stack_ctx Γ π1 π2)
           (aux : Aux Args Γ π1 π2 )
    : ConversionResult ( Σ (wfΣ : abstract_env_ext_rel X Σ), ws_cumul_pb_terms Σ (Γ,,, stack_context π1)
                         (decompose_stack π1).1
                         (decompose_stack π2).1) :=
    _isconv_args leq Γ π1 π2 hx aux with inspect (decompose_stack π1) := {
    | @exist (, θ1) with inspect (decompose_stack π2) := {
      | @exist (, θ2) with _isconv_args' leq Γ [] θ1 _ _ θ2 _ _ _ _ := {
        | Success h := yes ;
        | Error e h := no e
        }
      }
    }.
  Next Obligation.
    pose proof (decompose_stack_eq _ _ _ (eq_sym )). subst.
    eauto.
  Qed.
  Next Obligation.
    eapply decompose_stack_noStackApp. eauto.
  Qed.
  Next Obligation.
    pose proof (decompose_stack_eq _ _ _ (eq_sym )). subst.
    eauto.
  Qed.
  Next Obligation.
    eapply decompose_stack_noStackApp. eauto.
  Qed.
  Next Obligation.
    pose proof (decompose_stack_eq _ _ _ (eq_sym )). subst.
    pose proof (decompose_stack_eq _ _ _ (eq_sym )). subst.
    rewrite 2!stack_context_appstack in hx.
    eauto.
  Qed.
  Next Obligation.
    eapply (aux Reduction). all: auto.
    pose proof (decompose_stack_eq _ _ _ (eq_sym )). subst.
    instantiate (1 := ).
    simpl in . destruct as [eq hp].
    unshelve eapply R_positionR. 2: assumption.
    simpl. rewrite eq. reflexivity.
  Defined.
  Obligation Tactic := idtac.
  Next Obligation.
    intros; cbn in ×.
    rewrite (stack_context_decompose π1).
    rewrite , .
    auto.
  Qed.
  Next Obligation.
    intros; cbn in ×.
    rewrite (stack_context_decompose π1).
    rewrite , .
    auto.
  Qed.
  Obligation Tactic :=
    Tactics.program_simplify; CoreTactics.equations_simpl; try Tactics.program_solve_wf.

  Equations unfold_one_case (Γ : context) (ci : case_info)
            (p : predicate term) (c : term) (brs : list (branch term))
            (h : Σ (wfΣ : abstract_env_ext_rel X Σ), welltyped Σ Γ (tCase ci p c brs)) : option term :=
    unfold_one_case Γ ci p c brs h
    with inspect (reduce_stack RedFlags.default _ X Γ c [] _) := {
    | @exist (cred, ρ) eq with cc_viewc cred := {
      | ccview_construct ind' n ui with inspect (decompose_stack ρ) := {
        | @exist (args, ξ) eq' with inspect (nth_error brs n) := {
          | exist (Some br) eqbr := Some (iota_red ci.(ci_npar) p args br) ;
          | exist None eqbr := False_rect _ _ }
        } ;
      | ccview_cofix mfix idx with inspect (unfold_cofix mfix idx) := {
        | @exist (Some (narg, fn)) with inspect (decompose_stack ρ) := {
          | @exist (args, ξ) eq' := Some (tCase ci p (mkApps fn args) brs)
          } ;
        | @exist None := False_rect _ _
        } ;
      | ccview_other cred _ := None
      }
    }.
  Next Obligation.
    destruct ( _ wfΣ) as []. specialize_Σ wfΣ.
    cbn. destruct h as [T h].
    apply inversion_Case in h ; auto.
    destruct h as [mdecl [idecl [isdecl [indices [[] cum]]]]].
    eexists. eassumption.
  Qed.
  Next Obligation.
    destruct (abstract_env_ext_exists X) as [[Σ wfΣ]].
    simpl_reduce_stack Σ wfΣ.
    destruct ( _ wfΣ) as [].
    assert (r' : red Σ Γ (tCase ci p c brs)
      (tCase ci p (mkApps (tConstruct ind' n ui) (decompose_stack ρ).1) brs))
      by eapply red_case_c, r.
    pose proof (red_welltyped _ (h _ wfΣ) r') as h'.
    destruct h'.
    apply PCUICInductiveInversion.invert_Case_Construct in as (?&?&?&?); auto.
    congruence.
  Qed.

  Next Obligation.
    destruct (abstract_env_ext_exists X) as [[Σ wfΣ]].
    simpl_reduce_stack Σ wfΣ.
    destruct (h _ wfΣ) as (?&typ); auto.
    destruct ( _ wfΣ).
    apply inversion_Case in typ as [mdecl [idecl [isdecl [indices [[] cum]]]]]; auto.
    eapply PCUICSR.subject_reduction in scrut_ty. 2:auto. 2:exact r.
    eapply PCUICValidity.inversion_mkApps in scrut_ty as (?&typ&?); auto.
    apply inversion_CoFix in typ as (?&?&?&?&?&?&?); auto.
    unfold unfold_cofix in .
    rewrite e in .
    congruence.
  Qed.

  Lemma unfold_one_case_cored :
     Σ (wfΣ : abstract_env_ext_rel X Σ) Γ ci p c brs h t,
      Some t = unfold_one_case Γ ci p c brs h
      cored Σ Γ t (tCase ci p c brs).
  Proof using Type.
    intros Σ wfΣ Γ ci p c brs h t e.
    revert e.
    funelim (unfold_one_case Γ ci p c brs h).
    all:try Program.Tactics.bang.
    all: intros eq'' ; noconf eq''.
    - clear H .
      simpl_reduce_stack Σ wfΣ.
      destruct ( _ wfΣ) as [].
      assert (r' : red Σ Γ (tCase ci p c brs)
          (tCase ci p (mkApps (tConstruct ind' n ui) (decompose_stack ρ).1) brs))
        by eapply red_case_c, r.
      pose proof (red_welltyped _ (h _ wfΣ) r') as h'.
      eapply Case_Construct_ind_eq in h' ; eauto. subst.
      eapply cored_red_cored.
      + constructor. eapply red_iota. 1: now symmetry.
        destruct (h _ wfΣ) as (?&typ).
        eapply PCUICSR.subject_reduction in typ; eauto.
        apply PCUICInductiveInversion.invert_Case_Construct in typ as (?&?&?&?); auto.
        rewrite in eqbr; noconf eqbr. eauto.
      + eapply red_case_c, r.
    - clear H .
      simpl_reduce_stack Σ wfΣ.
      assert (r' : red Σ Γ (tCase ci p c brs)
                     (tCase ci p (mkApps (tCoFix mfix idx) (decompose_stack ρ).1) brs))
        by eapply red_case_c, r.
      destruct ( _ wfΣ) as [].
      pose proof (red_welltyped _ (h _ wfΣ) r') as h'.
      eapply cored_red_cored.
      + constructor. eapply red_cofix_case. eauto.
      + eapply red_case_c, r.
  Qed.


  Lemma unfold_one_case_None Σ (wfΣ : abstract_env_ext_rel X Σ) Γ ci p c brs h :
    None = unfold_one_case Γ ci p c brs h
     c', red Σ Γ c c' × whne RedFlags.default Σ Γ c'.
  Proof using Type.
    funelim (unfold_one_case Γ ci p c brs h); intros [=].
    - clear H.
      simpl_reduce_stack Σ wfΣ.
      destruct (h _ wfΣ) as (?&typ); auto.
      destruct ( _ wfΣ), w.
      constructor; (mkApps cred (decompose_stack ρ).1).
      split; [exact r|].
      specialize (isr eq_refl) as (noapp&_).
      eapply PCUICSR.subject_reduction in typ.
      2: eauto.
      2: eapply red_case_c, r.
      eapply whnf_case_arg_whne; eauto.
      now destruct cred.
    - match type of with
      | _ = False_rect _ ?fdestruct f
      end.
    - match type of with
      | _ = False_rect _ ?fdestruct f
      end.
  Qed.


  Equations unfold_one_proj (Γ : context) (p : projection) (c : term)
            (h : Σ (wfΣ : abstract_env_ext_rel X Σ), welltyped Σ Γ (tProj p c)) : option term :=

    unfold_one_proj Γ p c h with p := {
    | mkProjection i pars narg with inspect (reduce_stack RedFlags.default _ X Γ c [] _) := {
      | @exist (cred, ρ) eq with cc0_viewc cred := {
        | cc0view_construct ind' ui with inspect (decompose_stack ρ) := {
          | @exist (args, ξ) eq' with inspect (nth_error args (pars + narg)) := {
            | @exist (Some arg) := Some arg ;
            | @exist None := False_rect _ _
            }
          } ;
        | cc0view_cofix mfix idx with inspect (decompose_stack ρ) := {
          | @exist (args, ξ) eq' with inspect (unfold_cofix mfix idx) := {
            | @exist (Some (rarg, fn)) :=
              Some (tProj p (mkApps fn args)) ;
            | @exist None := False_rect _ _
            }
          } ;
        | cc0view_other cred _ := None
        }
      }
    }.
  Next Obligation.
    destruct ( _ wfΣ) as [].
    cbn. destruct (h _ wfΣ) as [T h'].
    apply inversion_Proj in h' ; auto.
    destruct h' as [uni [mdecl [idecl [pdecl [args' [? [? [? ?]]]]]]]].
    eexists. eassumption.
  Qed.
  Next Obligation.
    destruct (abstract_env_ext_exists X) as [[Σ wfΣ]].
    simpl_reduce_stack Σ wfΣ.
    destruct (h _ wfΣ) as (?&typ); auto.
    destruct ( _ wfΣ).
    eapply PCUICSR.subject_reduction in typ.
    2: auto.
    2: apply red_proj_c, r.
    apply PCUICInductiveInversion.invert_Proj_Construct in typ as (&_&?); auto.
    apply eq_sym, nth_error_None in . cbn in H.
    .
  Qed.
  Next Obligation.
    destruct (abstract_env_ext_exists X) as [[Σ wfΣ]].
    simpl_reduce_stack Σ wfΣ.
    destruct (h _ wfΣ) as (?&typ); auto.
    destruct ( _ wfΣ).
    apply inversion_Proj in typ as (?&?&?&?&?&?&?&?&?&?); auto.
    eapply PCUICSR.subject_reduction in t. 2:eauto. 2:exact r.
    apply PCUICValidity.inversion_mkApps in t as (?&?&?); auto.
    apply inversion_CoFix in t as (?&?&?&?&?&?&?); auto.
    unfold unfold_cofix in .
    rewrite in .
    congruence.
  Qed.

  Lemma unfold_one_proj_cored :
     Σ (wfΣ : abstract_env_ext_rel X Σ) Γ p c h t,
      Some t = unfold_one_proj Γ p c h
      cored Σ Γ t (tProj p c).
  Proof using Type.
    intros Σ wfΣ Γ p c h t e.
    revert e.
    funelim (unfold_one_proj Γ p c h).
    all: intros eq'' ; noconf eq''.
    - set (p := {| proj_ind := i; proj_npars := pars; proj_arg := narg |}).
       clear H .
      simpl_reduce_stack Σ wfΣ.
      pose proof (red_proj_c p _ _ r) as r'.
      destruct ( _ wfΣ) as [].
      pose proof (red_welltyped _ (h _ wfΣ) r') as h'.
      apply Proj_Construct_ind_eq in h' ; auto. subst.
      eapply cored_red_cored.
      + constructor. eapply (red_proj _ _ p). eauto.
      + eapply red_proj_c, r.
    - match type of eq'' with
      | _ = False_rect _ ?fdestruct f
      end.
    - set (p := {| proj_ind := i; proj_npars := pars; proj_arg := narg |}).
      clear H .
      simpl_reduce_stack Σ wfΣ.
      pose proof (red_proj_c p _ _ r) as r'.
      destruct ( _ wfΣ) as [].
      pose proof (red_welltyped _ (h _ wfΣ) r') as h'.
      eapply cored_red_cored.
      + constructor. eapply red_cofix_proj. eauto.
      + eapply red_proj_c, r.
    - match type of eq'' with
      | _ = False_rect _ ?fdestruct f
      end.
  Qed.


  Lemma unfold_one_proj_None Σ (wfΣ : abstract_env_ext_rel X Σ) Γ p c h :
    None = unfold_one_proj Γ p c h
     c', red Σ Γ c c' × whne RedFlags.default Σ Γ c'.
  Proof using Type.
    funelim (unfold_one_proj Γ p c h); intros [=].
    - clear H.
      simpl_reduce_stack Σ wfΣ.
      destruct ( _ wfΣ), w.
      destruct (h _ wfΣ) as (?&typ); auto.
      constructor; (mkApps cred (decompose_stack ρ).1).
      split; [exact r|].
      specialize (isr eq_refl) as (noapp&_).
      eapply PCUICSR.subject_reduction in typ.
      2: eauto.
      2: eapply red_proj_c, r.
      eapply whnf_proj_arg_whne ; eauto.
      now destruct cred.
    - match type of with
      | _ = False_rect _ ?fdestruct f
      end.
    - match type of with
      | _ = False_rect _ ?fdestruct f
      end.
  Qed.


  Equations reducible_head (Γ : context) (t : term) (π : stack)
            (h : wtp Γ t π)
    : option (term × stack) :=

    reducible_head Γ (tFix mfix idx) π h := unfold_one_fix Γ mfix idx π h ;

    reducible_head Γ (tCase ci p c brs) π h
    with inspect (unfold_one_case (Γ ,,, stack_context π) ci p c brs _) := {
    | @exist (Some t) eq :=Some (t, π) ;
    | @exist None _ := None
    } ;

    reducible_head Γ (tProj p c) π h
    with inspect (unfold_one_proj (Γ ,,, stack_context π) p c _) := {
    | @exist (Some t) eq := Some (t, π) ;
    | @exist None _ := None
    } ;

    reducible_head Γ (tConst c u) π h
    with inspect (abstract_env_lookup X c) := {
    | @exist (Some (ConstantDecl {| cst_body := Some body |})) eq :=
      Some (subst_instance u body, π) ;
    | @exist _ _ := None
    } ;

    reducible_head Γ _ π h := None.
  Next Obligation.
    zip fold in h.
    pose (abstract_env_ext_sq_wf _ X _ wfΣ).
    sq.
    eapply welltyped_context in h ; eauto.
  Qed.
  Next Obligation.
    pose (abstract_env_ext_sq_wf _ X _ wfΣ).
    sq.
    zip fold in h.
    eapply welltyped_context in h ; eauto.
  Qed.

  Lemma reducible_head_red_zipp :
     Σ (wfΣ : abstract_env_ext_rel X Σ) Γ t π h fn ξ,
      Some (fn, ξ) = reducible_head Γ t π h
       red (fst Σ) (Γ ,,, stack_context π) (zipp t π) (zipp fn ξ) .
  Proof using Type.
    intros Σ wfΣ Γ t π h fn ξ e.
    revert e.
    funelim (reducible_head Γ t π h).
    all: intro ee ; noconf ee.
    - eapply unfold_one_fix_red_zipp; eauto.
    - constructor. simpl_stacks.
      eapply red_mkApps_f.
      eapply trans_red.
      + reflexivity.
      + eapply red_delta.
      × unfold declared_constant.
        erewrite abstract_env_lookup_correct; eauto.
        × reflexivity.
    - eapply unfold_one_case_cored in eq as r; eauto.
      apply cored_red in r.
      destruct r as [r].
      constructor. simpl_stacks.
      eapply red_mkApps_f.
      assumption.
    - eapply unfold_one_proj_cored in eq as r; eauto.
      apply cored_red in r.
      destruct r as [r].
      constructor. simpl_stacks.
      eapply red_mkApps_f.
      assumption.
  Qed.


  Lemma reducible_head_red_zippx :
     Σ (wfΣ : abstract_env_ext_rel X Σ) Γ t π h fn ξ,
      Some (fn, ξ) = reducible_head Γ t π h
       red (fst Σ) Γ (zippx t π) (zippx fn ξ) .
  Proof using Type.
    intros Σ wfΣ Γ t π h fn ξ e.
    revert e.
    funelim (reducible_head Γ t π h).
    all: intro ee ; noconf ee.
    - eapply unfold_one_fix_red_zippx; eauto.
    - constructor. unfold zippx.
      case_eq (decompose_stack π). intros l s eq'.
      eapply red_it_mkLambda_or_LetIn. eapply red_mkApps_f.
      eapply trans_red.
      + reflexivity.
      + eapply red_delta.
        × unfold declared_constant.
          erewrite abstract_env_lookup_correct; eauto.
        × reflexivity.
    - eapply unfold_one_case_cored in eq as r; eauto. apply cored_red in r.
      destruct r as [r].
      constructor. unfold zippx.
      case_eq (decompose_stack π). intros l s e'.
      eapply red_it_mkLambda_or_LetIn. eapply red_mkApps_f.
      apply decompose_stack_eq in e'. subst.
      rewrite stack_context_appstack in r. assumption.
    - eapply unfold_one_proj_cored in eq as r;eauto. apply cored_red in r.
      destruct r as [r].
      constructor. unfold zippx.
      case_eq (decompose_stack π). intros l s e'.
      eapply red_it_mkLambda_or_LetIn. eapply red_mkApps_f.
      apply decompose_stack_eq in e'. subst.
      rewrite stack_context_appstack in r. assumption.
  Qed.


  Lemma reducible_head_cored :
     Σ (wfΣ : abstract_env_ext_rel X Σ) Γ t π h fn ξ,
      Some (fn, ξ) = reducible_head Γ t π h
      cored Σ Γ (zipc fn ξ) (zipc t π).
  Proof using Type.
    intros Σ wfΣ Γ t π h fn ξ e.
    revert e.
    funelim (reducible_head Γ t π h).
    all: intro ee ; noconf ee.
    - eapply unfold_one_fix_cored; eauto.
    - repeat zip fold. eapply cored_context.
      constructor. eapply red_delta.
      + unfold declared_constant.
        erewrite abstract_env_lookup_correct; eauto.
      + reflexivity.
    - repeat zip fold. eapply cored_context.
      eapply unfold_one_case_cored; eauto.
    - repeat zip fold. eapply cored_context.
      eapply unfold_one_proj_cored; eauto.
  Qed.


  Lemma reducible_head_decompose :
     Γ t π h fn ξ,
      Some (fn, ξ) = reducible_head Γ t π h
      snd (decompose_stack π) = snd (decompose_stack ξ).
  Proof using Type.
    intros Γ t π h fn ξ e.
    revert e.
    funelim (reducible_head Γ t π h).
    all: intro ee ; noconf ee.
    - eapply unfold_one_fix_decompose. eassumption.
    - reflexivity.
    - reflexivity.
    - reflexivity.
  Qed.



  Lemma reducible_head_None Σ (wfΣ : abstract_env_ext_rel X Σ) Γ t π h :
    isApp t = false
    whnf RedFlags.nodelta Σ (Γ,,, stack_context π) (mkApps t (decompose_stack π).1)
    None = reducible_head Γ t π h
     t' args',
      whnf_red Σ (Γ,,, stack_context π) t t' ×
       (red Σ (Γ,,, stack_context π)) (decompose_stack π).1 args' ×
      whnf RedFlags.default Σ (Γ,,, stack_context π) (mkApps t' args').
  Proof using Type.
    funelim (reducible_head Γ t π h); intros notapp wh [=].
    - apply whnf_mkApps_inv in wh.
      depelim wh; solve_discr.
      depelim w; solve_discr; try discriminate.
      constructor; eexists _, (decompose_stack π).1.
      split; [now constructor|].
      split; eauto with pcuic.
      apply whnf_mkApps.
      eauto with pcuic.
    - apply whnf_mkApps_inv in wh; auto.
      depelim wh; solve_discr.
      constructor; eexists _, (decompose_stack π).1.
      split; [constructor|].
      split; eauto with pcuic.
      apply whnf_mkApps.
      constructor.
    - apply whnf_mkApps_inv in wh; auto.
      depelim wh; solve_discr.
      constructor; eexists _, (decompose_stack π).1.
      split; [constructor; eauto with pcuic|].
      split; eauto with pcuic.
      apply whnf_mkApps.
      depelim w; solve_discr; eauto with pcuic.
    - apply whnf_mkApps_tSort_inv in wh as →.
      constructor; eexists _, [].
      eauto using whnf_red with pcuic.
    - apply whnf_mkApps_tProd_inv in wh as →.
      constructor; eexists _, [].
      eauto using whnf_red with pcuic.
    - depelim wh; solve_discr.
      + apply whne_mkApps_inv in w as [|(?&?&?&?&?&?&?&?&?)]; auto; try discriminate.
        depelim w; solve_discr.
        discriminate.
      + rewrite .
        constructor; eexists _, []; eauto using whnf_red with pcuic.
    - apply whnf_mkApps_inv in wh; auto.
      depelim wh; solve_discr.
      depelim w; solve_discr.
      discriminate.
    - discriminate.
    - constructor; eexists _, (decompose_stack π).1; eauto using whnf_red with pcuic.
    - constructor; eexists _, (decompose_stack π).1; eauto using whnf_red with pcuic.
    - eapply unfold_one_fix_None in as [(?&?&?)]; eauto.
      constructor; eexists _, x.
      split; [constructor; eauto with pcuic|].
      eauto with pcuic.
    - constructor; eexists _, (decompose_stack π).1.
      split; [constructor; eauto with pcuic|].
      eauto with pcuic.
    - constructor; eexists _, (decompose_stack π).1.
      clear H. erewrite abstract_env_lookup_correct in e; eauto.
      split; [econstructor|]; eauto.
      split; [eauto with pcuic|].
      apply whnf_mkApps.
      eapply whne_const; eauto.
    - zip fold in h.
      destruct ( _ wfΣ).
      eapply welltyped_context in h; eauto.
      destruct h as (?&typ); auto.
      apply inversion_Const in typ as (?&?&?&?); auto.
      unfold declared_constant in d.
      clear H. erewrite abstract_env_lookup_correct in e; eauto.
      congruence.
    - zip fold in h.
      destruct ( _ wfΣ).
      eapply welltyped_context in h; eauto.
      destruct h as (?&typ); auto.
      apply inversion_Const in typ as (?&?&?&?); auto.
      unfold declared_constant in d.
      clear H. erewrite abstract_env_lookup_correct in e; eauto.
      congruence.
    - clear H.
      eapply unfold_one_case_None in e as [(c'&r&whcase)]; eauto.
      constructor; (tCase ci p c' brs), (decompose_stack π).1.
      split.
      + destruct p. constructor; eauto with pcuic.
      + split; [eauto with pcuic|].
        apply whnf_mkApps.
        auto.
    - clear H.
      eapply unfold_one_proj_None in e as [(c'&r&whproj)]; eauto.
      constructor; (tProj p c'), (decompose_stack π).1.
      split.
      + constructor; eauto with pcuic.
      + split; [eauto with pcuic|].
        apply whnf_mkApps.
        auto.
  Qed.


  Equations(noeqns) _isconv_fallback (Γ : context) (leq : conv_pb)
            (t1 : term) (π1 : stack) (h1 : wtp Γ π1)
            (t2 : term) (π2 : stack) (h2 : wtp Γ π2)
            (ir1 : isred_full Γ π1) (ir2 : isred_full Γ π2)
            (hdiscr : prog_discr )
            (hx : conv_stack_ctx Γ π1 π2)
            (aux : Aux Fallback Γ π1 π2 )
    : ConversionResult (conv_term leq Γ π1 π2) :=
    _isconv_fallback Γ leq π1 π2 hdiscr hx aux
    with inspect (reducible_head Γ π1 ) := {
    | exist (Some (, ρ1)) with inspect (decompose_stack ρ1) := {
      | exist (, θ1)
        with inspect (reduce_stack RedFlags.nodelta _ X (Γ ,,, stack_context ρ1) (appstack []) _) := {
        | exist (, θ1') :=
          isconv_prog leq (θ1' θ1) π2 aux
        }
      } ;
    | exist None with inspect (reducible_head Γ π2 ) := {
      | exist (Some (, ρ2)) with inspect (decompose_stack ρ2) := {
        | exist (, θ2)
          with inspect (reduce_stack RedFlags.nodelta _ X (Γ ,,, stack_context ρ2) (appstack []) _) := {
          | exist (, θ2') :=
            isconv_prog leq π1 (θ2' θ2) aux
          }
        } ;
      | exist None with inspect (eqb_termp_napp_gen leq (abstract_env_eq X) (abstract_env_leq X) (abstract_env_compare_global_instance X) #|(decompose_stack π1).1| ) := {
        | exist true := isconv_args leq π1 π2 aux;
        | exist false noteq :=
          no (
              HeadMismatch
                leq
                (Γ ,,, stack_context π1)
                (Γ ,,, stack_context π2)
            )
        }
      }
    }.
  Next Obligation.
    eapply reducible_head_red_zipp in as r; eauto.
    pose proof ( := _ wfΣ).
    sq.
    apply reducible_head_decompose in as d.
    eapply welltyped_zipc_zipp in as ; eauto.
    cbn in ×.
    pose proof (red_welltyped _ r) as hh.
    simpl_stacks.
    assumption.
  Qed.
  Next Obligation.
    eapply reducible_head_cored in as ; eauto.
    apply cored_red in .
    pose proof ( _ wfΣ).
    sq.
    simpl_reduce_stack Σ wfΣ.
    eapply red_welltyped; revgoals. 3:auto.
    - zip fold. eapply red_context_zip. simpl_stacks. exact r.
    - cbn.
      simpl_stacks.
      eapply red_welltyped. 1:auto.
      2: exact .
      eauto.
  Qed.
  Next Obligation.
    eapply R_cored. simpl. intros.
    eapply reducible_head_cored in as ; eauto.
    apply reducible_head_decompose in as .
    rewrite in . cbn in .
    case_eq (decompose_stack π1). intros l' s' e'.
    rewrite e' in . cbn in . subst.
    match type of with
    | _ = reduce_stack ?f _ ?X ?Γ ?t ?π ?h
      destruct (reduce_stack_sound f _ X Σ wfΣ Γ t π h) as [] ;
      pose proof (reduce_stack_decompose RedFlags.nodelta _ X _ _ _ h) as
    end.
    rewrite in . cbn in .
    rewrite in . cbn in .
    rewrite decompose_stack_appstack in . cbn in .
    rewrite zipc_appstack in . cbn in .
    case_eq (decompose_stack θ1'). intros l s e.
    rewrite e in . cbn in . subst.
    apply decompose_stack_eq in e as ?. subst.
    apply decompose_stack_eq in e' as ?. subst.
    rewrite stack_cat_appstack. rewrite 2!zipc_appstack.
    rewrite zipc_appstack in . simpl in .
    clear . symmetry in . apply decompose_stack_eq in . subst.
    rewrite 2!zipc_appstack in .
    rewrite stack_context_appstack in .
    eapply red_cored_cored ; try eassumption.
    repeat zip fold. eapply red_context_zip, .
  Qed.
  Next Obligation.
    apply reducible_head_decompose in as .
    simpl_reduce_stack Σ H.
    eauto.
  Qed.
  Next Obligation.
    destruct (abstract_env_ext_exists X) as [[Σ wfΣ]].
    simpl_reduce_stack Σ wfΣ.
    specialize (isr eq_refl) as (?&_).
    split; auto. intros.
    erewrite (abstract_env_ext_irr _ _ wfΣ); eauto.
    now simpl_stacks.
    Unshelve. all: eauto.
  Qed.
  Next Obligation.
    eapply reducible_head_red_zipp in as ; eauto.
    destruct as [].
    apply reducible_head_decompose in as .
    simpl_reduce_stack Σ H.
    destruct ( _ H) as [].
    etransitivity ; try eauto.
    eapply red_conv_cum_l; try eauto.
    etransitivity ; try eassumption.
    eapply into_closed_red; tea.
    × fvs.
    × eapply (f_equal stack_context) in .
      rewrite !stack_context_decompose in . rewrite .
      now eapply wt_zip_mkapps.
  Unshelve. all:eauto.
  Qed.
  Next Obligation.
    apply h; clear h. intros Σ wfΣ.
    eapply reducible_head_red_zipp in as ; eauto.
    destruct as [].
    apply reducible_head_decompose in as .
    simpl_reduce_stack Σ wfΣ.
    destruct ( _ wfΣ) as [].
    etransitivity ; try eauto.
    eapply red_conv_cum_r ; try assumption.
    etransitivity; tea.
    eapply (f_equal stack_context) in .
    rewrite !stack_context_decompose in .
    eapply into_closed_red; [exact |..]. 1:fvs.
    rewrite . now eapply wt_zip_mkapps.
    Unshelve. all:eauto.
  Qed.
  Next Obligation.
    eapply reducible_head_red_zipp in as r; eauto.
    pose proof ( := _ wfΣ).
    sq.
    apply reducible_head_decompose in as d.
    cbn.
    eapply welltyped_zipc_zipp in as ; eauto.
    pose proof (red_welltyped _ r) as hh.
    simpl_stacks.
    assumption.
  Qed.
  Next Obligation.
    eapply reducible_head_cored in as ; eauto.
    apply cored_red in .
    pose proof ( := _ wfΣ).
    sq.
    match type of with
    | _ = reduce_stack ?f _ ?X ?Γ ?t ?π ?h
      destruct (reduce_stack_sound f _ X _ wfΣ Γ t π h) as [] ;
      pose proof (reduce_stack_decompose RedFlags.nodelta _ X _ _ _ h) as
    end.
    rewrite in . cbn in .
    rewrite in . cbn in .
    rewrite decompose_stack_appstack in . cbn in .
    rewrite zipc_appstack in . cbn in .
    case_eq (decompose_stack θ2'). intros l s e.
    rewrite e in . cbn in . subst.
    apply decompose_stack_eq in e as ?. subst.
    rewrite stack_cat_appstack.
    rewrite zipc_appstack in . cbn in .
    rewrite zipc_appstack.
    pose proof (eq_sym ) as .
    apply decompose_stack_eq in . subst.
    rewrite stack_context_appstack in .
    eapply red_welltyped; [auto|..] ; revgoals.
    - zip fold. eapply red_context_zip, .
    - rewrite zipc_appstack in . cbn.
      eapply red_welltyped; try apply ; eauto.
  Qed.
  Next Obligation.
    eapply R_cored2. all: simpl. all: try reflexivity.
    intros.
    eapply reducible_head_cored in as ; eauto.
    apply reducible_head_decompose in as .
    rewrite in . cbn in .
    case_eq (decompose_stack π2). intros l' s' e'.
    rewrite e' in . cbn in . subst.
    match type of with
    | _ = reduce_stack ?f _ ?X ?Γ ?t ?π ?h
      destruct (reduce_stack_sound f _ X _ wfΣ Γ t π h) as [] ;
      pose proof (reduce_stack_decompose RedFlags.nodelta _ X _ _ _ h) as
    end.
    rewrite in . cbn in .
    rewrite in . cbn in .
    rewrite decompose_stack_appstack in . cbn in .
    rewrite zipc_appstack in . cbn in .
    case_eq (decompose_stack θ2'). intros l s e.
    rewrite e in . cbn in . subst.
    apply decompose_stack_eq in e as ?. subst.
    apply decompose_stack_eq in e' as ?. subst.
    rewrite stack_cat_appstack. rewrite 2!zipc_appstack.
    rewrite zipc_appstack in . simpl in .
    clear . symmetry in . apply decompose_stack_eq in . subst.
    rewrite 2!zipc_appstack in .
    rewrite stack_context_appstack in .
    eapply red_cored_cored ; try eassumption.
    repeat zip fold. eapply red_context_zip, .
  Qed.
  Next Obligation.
    eapply reducible_head_decompose in as .
    now simpl_reduce_stack Σ H.
  Qed.
  Next Obligation.
    destruct (abstract_env_ext_exists X) as [[Σ wfΣ]];
    simpl_reduce_stack Σ wfΣ.
    specialize (isr eq_refl) as (?&_).
    split; auto. intros.
    erewrite (abstract_env_ext_irr _ _ wfΣ); eauto.
    now simpl_stacks.
    Unshelve. all: eauto.
  Qed.
  Next Obligation.
    destruct ( _ H) as [].
    eapply reducible_head_red_zipp in as ; eauto.
    destruct as [].
    apply reducible_head_decompose in as .
    simpl_reduce_stack Σ H.
    destruct (hx _ H) as [hx'].
    etransitivity ; try eauto.
    eapply conv_cum_conv_ctx.
    - eapply red_conv_cum_r.
      etransitivity; tea.
      eapply into_closed_red; [exact |..]. 1:fvs.
      eapply (f_equal stack_context) in .
      rewrite !stack_context_decompose in .
      eapply into_closed_red; [exact |..]. 1:fvs.
      rewrite . now eapply wt_zip_mkapps.
    - eauto.
    Unshelve. all:eauto.
  Qed.
  Next Obligation.
    apply h; clear h. intros Σ wfΣ.
    destruct ( _ wfΣ) as [].
    eapply reducible_head_red_zipp in as ; eauto.
    destruct as [].
    apply reducible_head_decompose in as .
    simpl_reduce_stack Σ wfΣ.
    destruct (hx _ wfΣ) as [hx'].
    etransitivity ; try eauto.
    eapply conv_cum_conv_ctx.
    - eapply red_conv_cum_l.
      etransitivity; tea.
      eapply (f_equal stack_context) in .
      rewrite !stack_context_decompose in .
      eapply into_closed_red; [exact |..]. 1:fvs.
      rewrite ; now eapply wt_zip_mkapps.
    - eauto.
    Unshelve. all:eauto.
  Qed.
  Next Obligation.
    eapply R_stateR. all: simpl. all: try reflexivity.
    constructor.
    Qed.

  Next Obligation.
    destruct (h _ H), ( _ H).
    eapply ws_cumul_pb_terms_alt in as (argsr&argsr'&[]).
    rewrite !zipp_as_mkApps.
    apply conv_cum_alt; auto.
    constructor; eexists _, _.
    constructor.
    - apply PCUICInductiveInversion.closed_red_mkApps; tea.
      × clear aux . eapply welltyped_zipc_zipp in ; fvs.
      × clear aux . eapply wt_zip_mkapps in ; eauto.
        rewrite on_free_vars_mkApps in . now apply andb_true_iff in .
    - apply PCUICInductiveInversion.closed_red_mkApps; tea.
      × clear aux . eapply welltyped_zipc_zipp in ; fvs.
      × clear aux . eapply wt_zip_mkapps in ; eauto.
        eapply wt_zip_mkapps in ; eauto. destruct (hx _ H).
        rewrite (All2_fold_length ).
        rewrite on_free_vars_mkApps in . now apply andb_true_iff in .
    - apply eq_term_upto_univ_napp_mkApps; auto.
      rewrite Nat.add_0_r.
      apply All2_length in a.
      rewrite a in .
      eapply eqb_term_upto_univ_impl with (q := closedu); eauto.
      + intros. eapply iff_reflect.
         eapply (abstract_env_compare_universe_correct _ H Conv) ; now eapply wf_universe_iff.
      + intros. eapply iff_reflect. destruct leq.
        × eapply (abstract_env_compare_universe_correct _ H Conv) ; now eapply wf_universe_iff.
        × eapply (abstract_env_compare_universe_correct _ H Cumul) ; now eapply wf_universe_iff.
      + intros. rewrite wf_universeb_instance_forall in ×.
        apply wf_universe_instance_iff in .
        apply wf_universe_instance_iff in .
        eapply (abstract_env_compare_global_instance_correct _ H); eauto.
        intros. apply ; now eapply wf_universe_iff.
      + pose proof as Hc. specialize_Σ H. pose proof ( _ H); sq.
        apply welltyped_zipc_inv in Hc; eauto.
        apply welltyped_wf in Hc; eauto.
      + pose proof as Hc. specialize_Σ H. pose proof ( _ H); sq.
        apply welltyped_zipc_inv in Hc; eauto.
        apply welltyped_wf in Hc; eauto.
  Qed.
  Next Obligation.
    apply h; clear h. intros Σ wfΣ.
    destruct as (&[whδ1]), as (&[whδ2]); eauto.
    erewrite !zipp_as_mkApps in ×.
    eapply reducible_head_None in as [(?&?&&&)]; eauto.
    eapply reducible_head_None in as [(?&?&&&)]; eauto.
    destruct ( _ wfΣ), (hx _ wfΣ).
    apply whnf_red_red in as ?.
    apply whnf_red_red in as ?.
    eapply conv_cum_red_conv_inv in H.
    2: eassumption.
    2: eassumption.
    2: eapply red_mkApps; eauto.
    2: apply red_mkApps; eauto.
    2: eauto.
    eapply conv_cum_mkApps_inv in H as [(?&?)]; eauto.
    2: now depelim .
    2: now depelim .
    2: eapply whnf_conv_context; eauto.
    2: symmetry in ; eapply ws_cumul_ctx_pb_forget in ; eauto.
    constructor.
    eapply ws_cumul_pb_terms_red_conv; eauto.
    all:eapply into_red_terms; tea.
    1:fvs. 2:fvs.
    all:clear aux.
    × eapply wt_zip_mkapps in ; eauto.
      rewrite on_free_vars_mkApps in . now apply andb_true_iff in as [].
    × eapply wt_zip_mkapps in ; eauto.
      rewrite on_free_vars_mkApps in . now apply andb_true_iff in as [].
  Qed.

  Next Obligation.
    unfold eqb_termp_napp in noteq.
    destruct (abstract_env_ext_exists X) as [[Σ wfΣ]].
    destruct as (&[whδ1]), as (&[whδ2]); eauto.
    erewrite !zipp_as_mkApps in ×.
    eapply reducible_head_None in as [(?&?&&&)]; eauto.
    eapply reducible_head_None in as [(?&?&&&)]; eauto.
    destruct ( _ wfΣ), (hx _ wfΣ).
    apply whnf_red_red in as ?.
    apply whnf_red_red in as ?.
    eapply conv_cum_red_conv_inv in H.
    2: eassumption.
    2: eassumption.
    2: apply red_mkApps; eassumption.
    2: apply red_mkApps; eassumption.
    2: eassumption.
    apply conv_cum_mkApps_inv in H as [(conv_hds&_)]; auto.
    2: now inversion ; subst.
    2: now inversion ; subst.
    2: eapply whnf_conv_context; eauto.
    2: { symmetry in . eapply ws_cumul_ctx_pb_forget in ; tea. }
    apply whnf_mkApps_inv in .
    destruct ; cbn in ×.
    all: inversion ; subst; clear .
    9: { destruct conv_hds as [H].
         inversion H; subst; clear H.
         inversion ; subst; clear .
         zip fold in .
         zip fold in .
         eapply welltyped_context in ; eauto.
         clear aux.
         eapply welltyped_context in ; eauto.
         destruct as (?&); auto.
         destruct as (?&); auto.
         apply inversion_Ind in as (?&?&?&?&?&?); auto.
         apply inversion_Ind in as (?&?&?&?&?&?); auto.
         apply consistent_instance_ext_wf in .
         apply consistent_instance_ext_wf in c.
         epose abstract_env_compare_global_instance_correct as Hcompare.
         eapply Hcompare in ; eauto.
         2: { intros; apply iff_reflect. eapply (abstract_env_compare_universe_correct _ _ leq); apply wf_universe_iff; eauto.
            all: apply wf_universe_iff; eauto.
         }
         rewrite eqb_refl in noteq.
         apply All2_length in .
         rewrite in .
         apply ssrbool.not_false_is_true. rewrite noteq.
         destruct leq; eauto.
}
    9: { destruct conv_hds as [H].
         inversion H; subst; clear H.
         inversion ; subst; clear .
         zip fold in .
         zip fold in .
         eapply welltyped_context in ; eauto.
         clear aux.
         eapply welltyped_context in ; eauto.
         destruct as (?&); auto.
         destruct as (?&); auto.
         apply inversion_Construct in as (?&?&?&?&?&?&?); auto.
         apply inversion_Construct in as (?&?&?&?&?&?&?); auto.
         apply consistent_instance_ext_wf in .
         apply consistent_instance_ext_wf in c.
         rewrite !eqb_refl in noteq.
         apply All2_length in .
         rewrite in .
         apply ssrbool.not_false_is_true. rewrite noteq. cbn.
         eapply abstract_env_compare_global_instance_correct; eauto.
         intros; apply iff_reflect.
         destruct leq; eapply abstract_env_compare_universe_correct; eauto.
         }
    all: apply conv_cum_alt in conv_hds as [(?&?&[ ?])]; auto.
    all: eapply whnf_red_inv in ; auto.
    all: inversion ; subst; clear .
    all: inversion c; subst; clear c.
    all: apply whnf_mkApps_inv in .
    all: eapply whnf_conv_context in ; [|symmetry in ; eapply ws_cumul_ctx_pb_forget in ; exact ].
    all: eapply whnf_red_inv in ; auto.
    all: inversion ; subst; clear .
    all: inversion ; subst; clear .
    all: destruct hdiscr.
    all: try now rewrite eqb_refl in noteq.
    - zip fold in .
      eapply welltyped_context in ; eauto.
      destruct as (?&typ).
      now apply inversion_Evar in typ.
    - zip fold in .
      zip fold in .
      eapply welltyped_context in as [ ]; eauto.
      clear aux.
      eapply welltyped_context in as [ ]; eauto.
      simpl in .
      apply inversion_Sort in as (_&&_); auto.
      apply inversion_Sort in as (_&&_); auto.
      eapply compare_universeb_complete in ; eauto.
      destruct leq; cbn in *; easy.
      Unshelve. all:eauto.
  Qed.

  Equations _isconv (s : state) (Γ : context)
            (t1 : term) (π1 : stack) (h1 : wtp Γ π1)
            (t2 : term) (π2 : stack) (h2 : wtp Γ π2)
            (aux : Aux s Γ π1 π2 )
  : Ret s Γ π1 π2 :=
    _isconv Reduction Γ π1 π2 aux :=
      λ { | leq | hx | _ | _ | _ := _isconv_red Γ leq π1 π2 hx aux } ;

    _isconv Term Γ π1 π2 aux :=
      λ { | leq | hx | | | _ := _isconv_prog Γ leq π1 π2 hx aux } ;

    _isconv Args Γ π1 π2 aux :=
      λ { | leq | hx | _ | _ | _ := _isconv_args leq Γ π1 π2 hx aux } ;

    _isconv Fallback Γ π1 π2 aux :=
      λ { | leq | hx | | | hd := _isconv_fallback Γ leq π1 π2 hd hx aux }.

  Derive Signature for dlexmod.

  Lemma welltyped_R_zipc Σ (wfΣ : abstract_env_ext_rel X Σ) Γ :
     x y : pack Γ, welltyped Σ Γ (zipc (tm1 x) (stk1 x)) R Γ y x welltyped Σ Γ (zipc (tm1 y) (stk1 y)).
  Proof using Type.
    intros x y H HR.
    pose proof (heΣ := heΣ _ wfΣ).
    pose proof ( := _ wfΣ). cbn.
    sq.
    destruct x, y; cbn in ×.
    depind HR.
    - cbn in ×. specialize_Σ wfΣ.
      eapply cored'_postpone in H as [u' [cor eq]].
      eapply cored_welltyped in cor; tea.
      destruct eq as [eq].
      eapply welltyped_alpha; tea. symmetry. exact eq.
    - simpl in ×. destruct e. eapply welltyped_alpha; tea.
      now symmetry.
  Qed.


  Equations(noeqns) isconv_full (s : state) (Γ : context)
            (t1 : term) (π1 : stack) (h1 : wtp Γ π1)
            (t2 : term) (π2 : stack) (h2 : wtp Γ π2)
    : Ret s Γ π1 π2 :=

    isconv_full s Γ π1 π2 hx :=
      Fix_F (R := R Γ)
            ( '(mkpack s' t1' π1' t2' π2' h2') ⇒
              wtp Γ π1'
              wtp Γ π2'
              Ret s' Γ π1' π2'
            )
            ( pp f_)
            (x := mkpack Γ s π1 π2 _)
            _ _ _ _.
  Next Obligation.
    unshelve eapply _isconv. all: try assumption.
    intros s' π1' π2' hx' hR.
    eapply (f (mkpack Γ s' π1' π2' )); tea.
    destruct pp. eapply R_irrelevance; tea; cbn. reflexivity.
  Defined.
  Next Obligation.
  match goal with | |- Acc _ ?Xset (u := X) end.
  revert .
  change (( Σ, abstract_env_ext_rel X Σ welltyped Σ Γ (zipc (tm1 u) (stk1 u))) Acc (R Γ) u).
  generalize u.
  refine (Acc_intro_generator
            (R:=R Γ)
            (P:= u Σ (wfΣ : abstract_env_ext_rel X Σ), welltyped Σ Γ (zipc (tm1 u) (stk1 u)))
            ( x y Px Hy_) 1000 _); intros.
  - simpl in ×. eapply welltyped_R_zipc; eauto.
  - destruct (abstract_env_ext_exists X) as [[Σ wfΣ]].
    destruct ( _ wfΣ) as []. eapply R_Acc; eassumption.
  Defined.

  Inductive ConversionResultSummary :=
  | ConvSuccess : ConversionResultSummary
  | ConvError : ConversionError ConversionResultSummary.

  Definition isconv Γ leq t1 π1 h1 t2 π2 h2 hx :=
    match isconv_full Reduction Γ π1 π2 leq hx I I I with
    | Success _ConvSuccess
    | Error e _ConvError e
    end.

  Theorem isconv_sound :
     Σ (wfΣ : abstract_env_ext_rel X Σ) Γ leq t1 π1 h1 t2 π2 h2 hx,
      isconv Γ leq π1 π2 hx = ConvSuccess
      conv_cum leq Σ (Γ ,,, stack_context π1) (zipp π1) (zipp π2).
  Proof using Type.
    unfold isconv.
    intros Σ wfΣ Γ leq π1 π2 hx.
    destruct isconv_full as [].
    - auto.
    - discriminate.
  Qed.


  Theorem isconv_complete :
     Σ (wfΣ : abstract_env_ext_rel X Σ) Γ leq t1 π1 h1 t2 π2 h2 hx e,
      isconv Γ leq π1 π2 hx = ConvError e
      ¬conv_cum leq Σ (Γ ,,, stack_context π1) (zipp π1) (zipp π2).
  Proof using Type.
    unfold isconv.
    intros Σ wfΣ Γ leq π1 π2 hx.
    destruct isconv_full as []; eauto.
    - intros ? [=].
    - intros. intro not; eapply h. intros.
      erewrite (abstract_env_ext_irr _ _ wfΣ) ; eauto.
      Unshelve. eauto.
  Qed.


  Program Definition isconv_term Γ leq t1 (h1 : Σ (wfΣ : abstract_env_ext_rel X Σ), welltyped Σ Γ ) t2 (h2 : Σ (wfΣ : abstract_env_ext_rel X Σ), welltyped Σ Γ ) :=
    isconv Γ leq [] [] _.

  Next Obligation.
    destruct ( _ H), ( _ H) as [].
    sq. eapply ws_cumul_ctx_pb_refl.
    fvs.
  Qed.

  Theorem isconv_term_sound :
     Σ (wfΣ : abstract_env_ext_rel X Σ) Γ leq t1 h1 t2 h2,
      isconv_term Γ leq = ConvSuccess
      conv_cum leq Σ Γ .
  Proof using Type.
    intros Σ wfΣ Γ leq .
    unfold isconv_term. intro h.
    eapply isconv_sound in h; eauto.
  Qed.


  Theorem isconv_term_complete :
     Σ (wfΣ : abstract_env_ext_rel X Σ) Γ leq t1 h1 t2 h2 e,
      isconv_term Γ leq = ConvError e
      ¬conv_cum leq Σ Γ .
  Proof using Type.
    intros Σ wfΣ Γ leq e.
    unfold isconv_term. intro h.
    eapply isconv_complete in h; eauto.
  Qed.

  Transparent reduce_stack.

End Conversion.