Module PSR := PCUICSafeReduce.

Definition global_uctx (Σ : global_env) : ContextSet.t
  := (global_levels Σ, global_constraints Σ).

Definition global_ext_uctx (Σ : global_env_ext) : ContextSet.t
  := (global_ext_levels Σ, global_ext_constraints Σ).

Definition wf_global_uctx_invariants {cf:checker_flags} Σ
  : ∥ wf Σ ∥ → global_uctx_invariants (global_uctx Σ).

Definition wf_ext_global_uctx_invariants {cf:checker_flags} Σ
  : ∥ wf_ext Σ ∥ → global_uctx_invariants (global_ext_uctx Σ).

Definition global_ext_uctx_consistent {cf:checker_flags} Σ
  : ∥ wf_ext Σ ∥ → consistent (global_ext_uctx Σ).2.
Qed.

Section Conversion.

  Context {cf : checker_flags}.
  Context (flags : RedFlags.t).
  Context (Σ : global_env_ext).
  Context (hΣ : ∥ wf Σ ∥) (Hφ : ∥ on_udecl Σ.1 Σ.2 ∥).
  Context (G : universes_graph) (HG : is_graph_of_uctx G (global_ext_uctx Σ)).



  Inductive state :=
  | Reduction (t : term)
  | Term (t : term)
  | Args
  | Fallback (t : term).

  Inductive stateR : state → state → Prop :=
  | stateR_Term_Reduction : ∀ u v, stateR (Term u) (Reduction v)
  | stateR_Args_Term : ∀ u, stateR Args (Term u)
  | stateR_Fallback_Term : ∀ u v, stateR (Fallback u) (Term v)
  | stateR_Args_Fallback : ∀ u, stateR Args (Fallback u).


  Lemma stateR_Acc :
    ∀ s, Acc stateR s.

  Notation wtp Γ t π :=
    (wellformed Σ Γ (zipc t π)) (only parsing).

  Definition wts Γ s t π :=
    match s with
    | Reduction t'
    | Fallback t'
    | Term t' ⇒ wtp Γ t' π
    | Args ⇒ wtp Γ t π
    end.


  Record pack (Γ : context) := mkpack {
    st : state ;
    tm : term ;
    stk1 : stack ;
    stk2 : stack ;
    tm' := match st with
           | Reduction t | Fallback t | Term t ⇒ t
           | Args ⇒ tm
           end ;
    wth : wellformed Σ Γ (zipc tm' stk2)
  }.


  Definition nlstate (s : state) :=
    match s with
    | Reduction t ⇒ Reduction (nl t)
    | Term t ⇒ Term (nl t)
    | Args ⇒ Args
    | Fallback t ⇒ Fallback (nl t)
    end.

  Definition nl_pack {Γ : context} (p : pack Γ) : pack (nlctx Γ).

  Definition wterm Γ := { t : term | wellformed Σ Γ t }.

  Definition wcored Γ (u v : wterm Γ) :=
    cored' Σ Γ (` u) (` v).

  Lemma wcored_wf :
    ∀ Γ, well_founded (wcored Γ).

  Definition eqt u v :=
    ∥ eq_term Σ u v ∥.

  Lemma eq_term_valid_pos :
    ∀ {u v p},
      validpos u p →
      eqt u v →
      validpos v p.


  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 \ cored' Σ Γ by _ ⨷
      @posR t ⊗
      w ⊨ weqt \ wcored Γ by _ ⨷
      @posR (` w) ⊗
      stateR.



  Lemma R_aux_Acc :
    ∀ Γ t p w q s,
      wellformed Σ Γ t →
      Acc (R_aux Γ) (t ; (p, (w ; (q, s)))).

  Notation pzt u := (zipc (tm u) (stk1 u)) (only parsing).
  Notation pps1 u := (stack_pos (tm u) (stk1 u)) (only parsing).
  Notation pwt u := (exist _ (wth u)) (only parsing).
  Notation pps2 u := (stack_pos (tm' 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,
      wellformed Σ Γ (zipc (tm u) (stk1 u)) →
      Acc (R Γ) u.

  Lemma R_cored :
    ∀ Γ p1 p2,
      cored Σ Γ (pzt p1) (pzt p2) →
      R Γ p1 p2.

  Lemma R_aux_positionR :
    ∀ Γ t1 t2 (p1 : pos t1) (p2 : pos t2) s1 s2,
      eq_term Σ t1 t2 →
      positionR (` p1) (` p2) →
      R_aux Γ (t1 ; (p1, s1)) (t2 ; (p2, s2)).

  Lemma R_positionR :
    ∀ Γ p1 p2,
      eq_term Σ (pzt p1) (pzt p2) →
      positionR (` (pps1 p1)) (` (pps1 p2)) →
      R Γ p1 p2.

  Lemma R_aux_cored2 :
    ∀ Γ t1 t2 (p1 : pos t1) (p2 : pos t2) w1 w2 q1 q2 s1 s2,
      eq_term Σ t1 t2 →
      ` p1 = ` p2 →
      cored' Σ Γ (` w1) (` w2) →
      R_aux Γ (t1 ; (p1, (w1 ; (q1, s1)))) (t2 ; (p2, (w2 ; (q2, s2)))).

  Lemma R_cored2 :
    ∀ Γ p1 p2,
      eq_term Σ (pzt p1) (pzt p2) →
      ` (pps1 p1) = ` (pps1 p2) →
      cored Σ Γ (` (pwt p1)) (` (pwt p2)) →
      R Γ p1 p2.

  Lemma R_aux_positionR2 :
    ∀ Γ t1 t2 (p1 : pos t1) (p2 : pos t2) w1 w2 q1 q2 s1 s2,
      eq_term Σ t1 t2 →
      ` p1 = ` p2 →
      eq_term Σ (` w1) (` w2) →
      positionR (` q1) (` q2) →
      R_aux Γ (t1 ; (p1, (w1 ; (q1, s1)))) (t2 ; (p2, (w2 ; (q2, s2)))).

  Lemma R_positionR2 :
    ∀ Γ p1 p2,
      eq_term Σ (pzt p1) (pzt p2) →
      ` (pps1 p1) = ` (pps1 p2) →
      eq_term Σ (` (pwt p1)) (` (pwt p2)) →
      positionR (` (pps2 p1)) (` (pps2 p2)) →
      R Γ p1 p2.

  Lemma R_aux_stateR :
    ∀ Γ t1 t2 (p1 : pos t1) (p2 : pos t2) w1 w2 q1 q2 s1 s2 ,
      eq_term Σ t1 t2 →
      ` p1 = ` p2 →
      eq_term Σ (` w1) (` w2) →
      ` q1 = ` q2 →
      stateR s1 s2 →
      R_aux Γ (t1 ; (p1, (w1 ; (q1, s1)))) (t2 ; (p2, (w2 ; (q2, s2)))).

  Lemma R_stateR :
    ∀ Γ p1 p2,
      eq_term Σ (pzt p1) (pzt p2) →
      ` (pps1 p1) = ` (pps1 p2) →
      eq_term Σ (` (pwt p1)) (` (pwt p2)) →
      ` (pps2 p1) = ` (pps2 p2) →
      stateR (st p1) (st p2) →
      R Γ p1 p2.

  Lemma eqb_term_upto_univ_refl :
    ∀ (eqb leqb : universe → universe → bool) t,
      (∀ u, eqb u u) →
      (∀ u, leqb u u) →
      eqb_term_upto_univ eqb leqb t t.

  Definition leqb_term :=
    eqb_term_upto_univ (try_eqb_universe G) (try_leqb_universe G).

  Definition eqb_term :=
    eqb_term_upto_univ (try_eqb_universe G) (try_eqb_universe G).

  Lemma leqb_term_spec t u :
    leqb_term t u →
    leq_term (global_ext_constraints Σ) t u.

  Lemma eqb_term_spec t u :
    eqb_term t u →
    eq_term (global_ext_constraints Σ) t u.

  Lemma leqb_term_refl :
    ∀ t, leqb_term t t.

  Lemma eqb_term_refl :
    ∀ t, eqb_term t t.

  Fixpoint eqb_ctx (Γ Δ : context) : bool :=
    match Γ, Δ with
    | [], [] ⇒ true
    | {| decl_name := na1 ; decl_body := None ; decl_type := t1 |} :: Γ,
      {| decl_name := na2 ; decl_body := None ; decl_type := t2 |} :: Δ ⇒
      eqb_term t1 t2 && eqb_ctx Γ Δ
    | {| decl_name := na1 ; decl_body := Some b1 ; decl_type := t1 |} :: Γ,
      {| decl_name := na2 ; decl_body := Some b2 ; decl_type := t2 |} :: Δ ⇒
      eqb_term b1 b2 && eqb_term t1 t2 && eqb_ctx Γ Δ
    | _, _ ⇒ false
    end.

  Lemma eqb_ctx_spec :
    ∀ Γ Δ,
      eqb_ctx Γ Δ →
      eq_context_upto (eq_universe (global_ext_constraints Σ)) Γ Δ.

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

  Lemma eqb_term_stack_spec :
    ∀ Γ t1 π1 t2 π2,
      eqb_term_stack t1 π1 t2 π2 →
      eq_context_upto (eq_universe (global_ext_constraints Σ))
                      (Γ ,,, stack_context π1)
                      (Γ ,,, stack_context π2) ×
      eq_term (global_ext_constraints Σ) (zipp t1 π1) (zipp t2 π2).

  Definition leqb_term_stack t1 π1 t2 π2 :=
    eqb_ctx (stack_context π1) (stack_context π2) &&
    leqb_term (zipp t1 π1) (zipp t2 π2).

  Definition eqb_termp leq u v :=
    match leq with
    | Conv ⇒ eqb_term u v
    | Cumul ⇒ leqb_term u v
    end.

  Lemma eqb_termp_spec :
    ∀ leq u v Γ,
      eqb_termp leq u v →
      conv leq Σ Γ u v.

  Lemma leqb_term_stack_spec :
    ∀ Γ t1 π1 t2 π2,
      leqb_term_stack t1 π1 t2 π2 →
      eq_context_upto (eq_universe (global_ext_constraints Σ))
                      (Γ ,,, stack_context π1)
                      (Γ ,,, stack_context π2) ×
      leq_term (global_ext_constraints Σ) (zipp t1 π1) (zipp t2 π2).

  Lemma zwts :
    ∀ {Γ s t π},
      wts Γ s t π →
      wellformed Σ Γ (zipc match s with Reduction u | Fallback u | Term u ⇒ u | Args ⇒ t end π).

  Notation conv_stack_ctx Γ π1 π2 :=
    (∥ conv_context Σ (Γ ,,, stack_context π1) (Γ ,,, stack_context π2) ∥).

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

  Notation alt_conv_term Γ t π π' :=
    (∥ Σ ;;; Γ ,,, stack_context π |- zipp t π == zipp t π' ∥)
      (only parsing).


  Definition Ret (s : state) Γ t π π' :=
    ∀ (leq : match s with Args ⇒ unit | _ ⇒ conv_pb end),
      conv_stack_ctx Γ π π' →
      (match s with Fallback t' | Term t' ⇒ isred (t, π) | _ ⇒ True end) →
      (match s with Fallback t' | Term t' ⇒ isred (t', π') | _ ⇒ True end) →
      { b : bool | match s
                return ∀ (leq : match s with Args ⇒ unit | _ ⇒ conv_pb end), Prop
                with
                | Reduction t' ⇒ fun leq ⇒
                  if b then conv_term leq Γ t π t' π' else True
                | Fallback t'
                | Term t' ⇒ fun leq ⇒
                  if b then conv_term leq Γ t π t' π' else True
                | Args ⇒ fun _ ⇒
                  if b then alt_conv_term Γ t π π' else True
                end leq
      }.

  Definition Aux s Γ t π1 π2 h2 :=
     ∀ s' t' π1' π2'
       (h1' : wtp Γ t' π1')
       (h2' : wts Γ s' t' π2'),
       conv_stack_ctx Γ π1 π2 →
       R Γ
         (mkpack Γ s' t' π1' π2' (zwts h2'))
         (mkpack Γ s t π1 π2 (zwts h2)) →
       Ret s' Γ t' π1' π2'.

  Notation no := (exist false I) (only parsing).
  Notation yes := (exist true _) (only parsing).

  Notation repack e := (let '(exist b h) := e in exist b _) (only parsing).

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

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


  Equations(noeqns) _isconv_red (Γ : context) (leq : conv_pb)
            (t1 : term) (π1 : stack) (h1 : wtp Γ t1 π1)
            (t2 : term) (π2 : stack) (h2 : wtp Γ t2 π2)
            (hx : conv_stack_ctx Γ π1 π2)
            (aux : Aux (Reduction t2) Γ t1 π1 π2 h2)
    : { b : bool | if b then conv_term leq Γ t1 π1 t2 π2 else True } :=

    _isconv_red Γ leq t1 π1 h1 t2 π2 h2 hx aux
    with inspect (decompose_stack π1) := {
    | @exist (args1, ρ1) e1 with inspect (decompose_stack π2) := {
      | @exist (args2, ρ2) e2
        with inspect (reduce_stack nodelta_flags Σ hΣ (Γ ,,, stack_context π1) t1 (appstack args1 ε) _) := {
        | @exist (t1',π1') eq1
          with inspect (reduce_stack nodelta_flags Σ hΣ (Γ ,,, stack_context π2) t2 (appstack args2 ε) _) := {
          | @exist (t2',π2') eq2 ⇒ isconv_prog leq t1' (π1' +++ ρ1) t2' (π2' +++ ρ2) aux
          }
        }
      }
    }.

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

    unfold_one_fix Γ mfix idx π h with inspect (unfold_fix mfix idx) := {
    | @exist (Some (arg, fn)) eq1 with inspect (decompose_stack_at π arg) := {
      | @exist (Some (l, c, θ)) eq2 with inspect (reduce_stack RedFlags.default Σ hΣ (Γ ,,, stack_context θ) c ε _) := {
        | @exist (cred, ρ) eq3 with construct_viewc cred := {
          | view_construct ind n ui := Some (fn, appstack l (App (zipc (tConstruct ind n ui) ρ) θ)) ;
          | view_other t h := None
          }
        } ;
      | _ := None
      } ;
    | _ := None
    }.


  Lemma unfold_one_fix_red_zipp :
    ∀ Γ mfix idx π h fn ξ,
      Some (fn, ξ) = unfold_one_fix Γ mfix idx π h →
      ∥ red (fst Σ) (Γ ,,, stack_context π) (zipp (tFix mfix idx) π) (zipp fn ξ) ∥.

  Lemma unfold_one_fix_red_zippx :
    ∀ Γ mfix idx π h fn ξ,
      Some (fn, ξ) = unfold_one_fix Γ mfix idx π h →
      ∥ red (fst Σ) Γ (zippx (tFix mfix idx) π) (zippx fn ξ) ∥.

  Lemma unfold_one_fix_red :
    ∀ Γ mfix idx π h fn ξ,
      Some (fn, ξ) = unfold_one_fix Γ mfix idx π h →
      ∥ red (fst Σ) Γ (zipc (tFix mfix idx) π) (zipc fn ξ) ∥.

  Lemma unfold_one_fix_cored :
    ∀ Γ mfix idx π h fn ξ,
      Some (fn, ξ) = unfold_one_fix Γ mfix idx π h →
      cored (fst Σ) Γ (zipc fn ξ) (zipc (tFix mfix idx) π).

  Lemma unfold_one_fix_decompose :
    ∀ Γ mfix idx π h fn ξ,
      Some (fn, ξ) = unfold_one_fix Γ mfix idx π h →
      snd (decompose_stack π) = snd (decompose_stack ξ).

  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.

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

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

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

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

  | prog_view_Case ind par p c brs ind' par' p' c' brs' :
      prog_view (tCase (ind, par) p c brs) (tCase (ind', par') p' c' brs')

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

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

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

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

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

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

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

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

    prog_viewc (tCase (ind, par) p c brs) (tCase (ind', par') p' c' brs') :=
      prog_view_Case ind par p c brs ind' par' 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 elimT (P : Type) (b : bool) : reflectT P b → b → P.

  Lemma introT (P : Type) (b : bool) : reflectT P b → P → b.

  Lemma wellformed_wf_local Γ t : wellformed Σ Γ t → ∥ wf_local Σ Γ ∥.

  Equations(noeqns) unfold_constants (Γ : context) (leq : conv_pb)
            (c : kername) (u : universe_instance) (π1 : stack)
            (h1 : wtp Γ (tConst c u) π1)
            (c' : kername) (u' : universe_instance) (π2 : stack)
            (h2 : wtp Γ (tConst c' u') π2)
            (hx : conv_stack_ctx Γ π1 π2)
            (aux : Aux (Term (tConst c' u')) Γ (tConst c u) π1 π2 h2)
    : { b : bool | if b then conv_term leq Γ (tConst c u) π1 (tConst c' u') π2 else True } :=

    unfold_constants Γ leq c u π1 h1 c' u' π2 h2 hx aux
    with inspect (lookup_env Σ c') := {
    | @exist (Some (ConstantDecl n {| cst_body := Some b |})) eq1 :=
      isconv_red leq (tConst c u) π1 (subst_instance_constr u' b) π2 aux ;
    
    | _ with inspect (lookup_env Σ c) := {
      | @exist (Some (ConstantDecl n {| cst_body := Some b |})) eq1 :=
        isconv_red leq (subst_instance_constr u b) π1
                        (tConst c' u') π2 aux ;
      
      | _ := no
      }
    }.

  Definition eqb_universe_instance u v :=
    forallb2 (try_eqb_universe G) (map Universe.make u) (map Universe.make v).

  Lemma eqb_universe_instance_spec :
    ∀ u v,
      eqb_universe_instance u v →
      R_universe_instance (eq_universe (global_ext_constraints Σ)) u v.

  Lemma wellformed_eq_term :
    ∀ Γ u v,
      wellformed Σ Γ u →
      eq_term Σ u v →
      wellformed Σ Γ v.

  Equations(noeqns) _isconv_prog (Γ : context) (leq : conv_pb)
            (t1 : term) (π1 : stack) (h1 : wtp Γ t1 π1)
            (t2 : term) (π2 : stack) (h2 : wtp Γ t2 π2)
            (hx : conv_stack_ctx Γ π1 π2)
            (ir1 : isred (t1, π1)) (ir2 : isred (t2, π2))
            (aux : Aux (Term t2) Γ t1 π1 π2 h2)
    : { b : bool | if b then conv_term leq Γ t1 π1 t2 π2 else True } :=

    _isconv_prog Γ leq t1 π1 h1 t2 π2 h2 hx ir1 ir2 aux with prog_viewc t1 t2 := {
    | prog_view_App _ _ _ _ :=
      False_rect _ _ ;

    | prog_view_Const c u c' u' with eq_dec c c' := {
      | left eq1 with inspect (eqb_universe_instance u u') := {
        | @exist true eq2 with isconv_args_raw (tConst c u) π1 π2 aux := {
          | @exist true h := yes ;
          
          | @exist false _ with inspect (lookup_env Σ c) := {
            | @exist (Some (ConstantDecl n {| cst_body := Some body |})) eq3 :=
              isconv_red leq (subst_instance_constr u body) π1
                             (subst_instance_constr u body) π2 aux ;
            
            | @exist _ _ := no
            }
          } ;
        
        | @exist false _ := unfold_constants Γ leq c u π1 h1 c' u' π2 h2 hx aux
        } ;
      
      | right _ := unfold_constants Γ leq c u π1 h1 c' u' π2 h2 hx aux
      } ;

    | prog_view_Lambda na A1 t1 na' A2 t2
      with isconv_red_raw Conv A1 (Lambda_ty na t1 π1)
                                 A2 (Lambda_ty na' t2 π2) aux := {
      | @exist true h :=
        isconv_red leq
                   t1 (Lambda_tm na A1 π1)
                   t2 (Lambda_tm na' A2 π2) aux ;
      | @exist false _ := no
      } ;

    | prog_view_Prod na A1 B1 na' A2 B2
      with isconv_red_raw Conv A1 (Prod_l na B1 π1) A2 (Prod_l na' B2 π2) aux := {
      | @exist true h :=
        isconv_red leq
                   B1 (Prod_r na A1 π1)
                   B2 (Prod_r na' A2 π2) aux ;
      | @exist false _ := no
      } ;

    | prog_view_Case ind par p c brs ind' par' p' c' brs'
      with inspect (eqb_term (tCase (ind, par) p c brs) (tCase (ind', par') p' c' brs')) := {
      | @exist true eq1 := isconv_args (tCase (ind, par) p c brs) π1 π2 aux ;
      | @exist false _ with inspect (reduce_term RedFlags.default Σ hΣ (Γ ,,, stack_context π1) c _) := {
        | @exist cred eq1 with inspect (reduce_term RedFlags.default Σ hΣ (Γ ,,, stack_context π2) c' _) := {
           | @exist cred' eq2 with inspect (eqb_term cred c && eqb_term cred' c') := {
              | @exist true eq3 := no ;
              | @exist false eq3 :=
                isconv_red leq (tCase (ind, par) p cred brs) π1
                               (tCase (ind', par') p' cred' brs') π2 aux
              }
           }
        }
      } ;

    | prog_view_Proj p c p' c' with inspect (eqb_term (tProj p c) (tProj p' c')) := {
      | @exist true eq1 := isconv_args (tProj p c) π1 π2 aux ;
      | @exist false _ := no
      } ;

    | prog_view_Fix mfix idx mfix' idx'
      with inspect (eqb_term (tFix mfix idx) (tFix mfix' idx')) := {
      | @exist true eq1 := isconv_args (tFix mfix idx) π1 π2 aux ;
      | @exist false _ with inspect (unfold_one_fix Γ mfix idx π1 _) := {
        | @exist (Some (fn, θ)) eq1
          with inspect (decompose_stack θ) := {
          | @exist (l', θ') eq2
            with inspect (reduce_stack nodelta_flags Σ hΣ (Γ ,,, stack_context θ') fn (appstack l' ε) _) := {
            | @exist (fn', ρ) eq3 :=
              isconv_prog leq fn' (ρ +++ θ') (tFix mfix' idx') π2 aux
            }
          } ;
        | _ with inspect (unfold_one_fix Γ mfix' idx' π2 _) := {
          | @exist (Some (fn, θ)) eq1
            with inspect (decompose_stack θ) := {
            | @exist (l', θ') eq2
              with inspect (reduce_stack nodelta_flags Σ hΣ (Γ ,,, stack_context θ') fn (appstack l' ε) _) := {
              | @exist (fn', ρ) eq3 :=
                isconv_prog leq (tFix mfix idx) π1 fn' (ρ +++ θ') aux
              }
            } ;
          | _ := no
          }
        }
      } ;

    | prog_view_CoFix mfix idx mfix' idx'
      with inspect (eqb_term (tCoFix mfix idx) (tCoFix mfix' idx')) := {
      | @exist true eq1 := isconv_args (tCoFix mfix idx) π1 π2 aux ;
      | @exist false _ := no
      } ;

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










  Definition Aux' Γ t args l1 π1 π2 h2 :=
     ∀ u1 u2 ca1 a1 ρ2
       (h1' : wtp Γ u1 (coApp (mkApps t ca1) (appstack a1 π1)))
       (h2' : wtp Γ u2 ρ2),
       let x := mkpack Γ (Reduction u2) u1 (coApp (mkApps t ca1) (appstack a1 π1)) ρ2 h2' in
       let y := mkpack Γ Args (mkApps t args) (appstack l1 π1) π2 h2 in
       (S #|ca1| + #|a1| = #|args| + #|l1|)%nat →
       pzt x = pzt y ∧
       positionR (` (pps1 x)) (` (pps1 y)) →
       Ret (Reduction u2) Γ u1 (coApp (mkApps t ca1) (appstack a1 π1)) ρ2.

  Equations(noeqns) _isconv_args' (Γ : context) (t : term) (args : list term)
            (l1 : list term) (π1 : stack)
            (h1 : wtp Γ (mkApps t args) (appstack l1 π1))
            (hπ1 : isStackApp π1 = false)
            (l2 : list term) (π2 : stack)
            (h2 : wtp Γ (mkApps t args) (appstack l2 π2))
            (hπ2 : isStackApp π2 = false)
            (hx : conv_stack_ctx Γ π1 π2)
            (aux : Aux' Γ t args l1 π1 (appstack l2 π2) h2)
    : { b : bool | if b then alt_conv_term Γ (mkApps t args) (appstack l1 π1) (appstack l2 π2) else True } by struct l1 :=
    _isconv_args' Γ t args (u1 :: l1) π1 h1 hπ1 (u2 :: l2) π2 h2 hπ2 hx aux
    with aux u1 u2 args l1 (coApp (mkApps t args) (appstack l2 π2)) _ _ _ _ Conv _ I I := {
    | @exist true H1 with _isconv_args' Γ t (args ++ [u1]) l1 π1 _ _ l2 π2 _ _ _ _ := {
      | @exist true H2 := yes ;
      | @exist false _ := no
      } ;
    | @exist false _ := no
    } ;

    _isconv_args' Γ t args [] π1 h1 hπ1 [] π2 h2 hπ2 hx aux := yes ;

    _isconv_args' Γ t args l1 π1 h1 hπ1 l2 π2 h2 hπ2 hx aux := no.

  Equations(noeqns) _isconv_args (Γ : context) (t : term)
           (π1 : stack) (h1 : wtp Γ t π1)
           (π2 : stack) (h2 : wtp Γ t π2)
           (hx : conv_stack_ctx Γ π1 π2)
           (aux : Aux Args Γ t π1 π2 h2)
    : { b : bool | if b then alt_conv_term Γ t π1 π2 else True } :=
    _isconv_args Γ t π1 h1 π2 h2 hx aux with inspect (decompose_stack π1) := {
    | @exist (l1, θ1) eq1 with inspect (decompose_stack π2) := {
      | @exist (l2, θ2) eq2 with _isconv_args' Γ t [] l1 θ1 _ _ l2 θ2 _ _ _ _ := {
        | @exist true h := yes ;
        | @exist false _ := no
        }
      }
    }.

  Equations unfold_one_case (Γ : context) (ind : inductive) (par : nat)
            (p c : term) (brs : list (nat × term))
            (h : wellformed Σ Γ (tCase (ind, par) p c brs)) : option term :=
    unfold_one_case Γ ind par p c brs h
    with inspect (reduce_stack RedFlags.default Σ hΣ Γ c ε _) := {
    | @exist (cred, ρ) eq with cc_viewc cred := {
      | ccview_construct ind' n ui with inspect (decompose_stack ρ) := {
        | @exist (args, ξ) eq' := Some (iota_red par n args brs)
        } ;
      | ccview_cofix mfix idx with inspect (unfold_cofix mfix idx) := {
        | @exist (Some (narg, fn)) eq2 with inspect (decompose_stack ρ) := {
          | @exist (args, ξ) eq' := Some (tCase (ind, par) p (mkApps fn args) brs)
          } ;
        | @exist None eq2 := None
        } ;
      | ccview_other t _ := None
      }
    }.

  Lemma unfold_one_case_cored :
    ∀ Γ ind par p c brs h t,
      Some t = unfold_one_case Γ ind par p c brs h →
      cored Σ Γ t (tCase (ind, par) p c brs).

  Equations unfold_one_proj (Γ : context) (p : projection) (c : term)
            (h : wellformed Σ Γ (tProj p c)) : option term :=

    unfold_one_proj Γ p c h with p := {
    | (i, pars, narg) with inspect (reduce_stack RedFlags.default Σ hΣ Γ c ε _) := {
      | @exist (cred, ρ) eq with cc_viewc cred := {
        | ccview_construct ind' n ui with inspect (decompose_stack ρ) := {
          | @exist (args, ξ) eq' with inspect (nth_error args (pars + narg)) := {
            | @exist (Some arg) eq2 := Some arg ;
            | @exist None _ := None
            }
          } ;
        | ccview_cofix mfix idx with inspect (decompose_stack ρ) := {
          | @exist (args, ξ) eq' with inspect (unfold_cofix mfix idx) := {
            | @exist (Some (narg, fn)) eq2 :=
              Some (tProj (i, pars, narg) (mkApps fn args)) ;
            | @exist None eq2 := None
            }
          } ;
        | ccview_other t _ := None
        }
      }
    }.

  Lemma unfold_one_proj_cored :
    ∀ Γ p c h t,
      Some t = unfold_one_proj Γ p c h →
      cored Σ Γ t (tProj p c).

  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 (ind, par) p c brs) π h
    with inspect (unfold_one_case (Γ ,,, stack_context π) ind par 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 (lookup_env Σ c) := {
    | @exist (Some (ConstantDecl _ {| cst_body := Some body |})) eq :=
      Some (subst_instance_constr u body, π) ;
    | @exist _ _ := None
    } ;

    reducible_head Γ _ π h := None.

  Lemma reducible_head_red_zipp :
    ∀ Γ t π h fn ξ,
      Some (fn, ξ) = reducible_head Γ t π h →
      ∥ red (fst Σ) (Γ ,,, stack_context π) (zipp t π) (zipp fn ξ) ∥.

  Lemma reducible_head_red_zippx :
    ∀ Γ t π h fn ξ,
      Some (fn, ξ) = reducible_head Γ t π h →
      ∥ red (fst Σ) Γ (zippx t π) (zippx fn ξ) ∥.

  Lemma reducible_head_cored :
    ∀ Γ t π h fn ξ,
      Some (fn, ξ) = reducible_head Γ t π h →
      cored Σ Γ (zipc fn ξ) (zipc t π).

  Lemma reducible_head_decompose :
    ∀ Γ t π h fn ξ,
      Some (fn, ξ) = reducible_head Γ t π h →
      snd (decompose_stack π) = snd (decompose_stack ξ).

  Equations(noeqns) _isconv_fallback (Γ : context) (leq : conv_pb)
            (t1 : term) (π1 : stack) (h1 : wtp Γ t1 π1)
            (t2 : term) (π2 : stack) (h2 : wtp Γ t2 π2)
            (ir1 : isred (t1, π1)) (ir2 : isred (t2, π2))
            (hx : conv_stack_ctx Γ π1 π2)
            (aux : Aux (Fallback t2) Γ t1 π1 π2 h2)
    : { b : bool | if b then conv_term leq Γ t1 π1 t2 π2 else True } :=
    _isconv_fallback Γ leq t1 π1 h1 t2 π2 h2 ir1 ir2 hx aux
    with inspect (reducible_head Γ t1 π1 h1) := {
    | @exist (Some (rt1, ρ1)) eq1 with inspect (decompose_stack ρ1) := {
      | @exist (l1, θ1) eq2
        with inspect (reduce_stack nodelta_flags Σ hΣ (Γ ,,, stack_context ρ1) rt1 (appstack l1 ε) _) := {
        | @exist (rt1', θ1') eq3 :=
          isconv_prog leq rt1' (θ1' +++ θ1) t2 π2 aux
        }
      } ;
    | @exist None _ with inspect (reducible_head Γ t2 π2 h2) := {
      | @exist (Some (rt2, ρ2)) eq1 with inspect (decompose_stack ρ2) := {
        | @exist (l2, θ2) eq2
          with inspect (reduce_stack nodelta_flags Σ hΣ (Γ ,,, stack_context ρ2) rt2 (appstack l2 ε) _) := {
          | @exist (rt2', θ2') eq3 :=
            isconv_prog leq t1 π1 rt2' (θ2' +++ θ2) aux
          }
        } ;
      | @exist None _ with inspect leq := {
        | @exist Conv eq1 with inspect (eqb_term t1 t2) := {
          | @exist true eq2 := isconv_args t1 π1 π2 aux ;
          | @exist false _ := no
          } ;
        | @exist Cumul eq1 with inspect (eqb_term t1 t2) := {
          | @exist true eq2 := isconv_args t1 π1 π2 aux ;
          | @exist false _ := exist (leqb_term (zipp t1 π1) (zipp t2 π2)) _
          }
        }
      }
    }.

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

    _isconv (Term t2) Γ t1 π1 h1 π2 h2 aux :=
      λ { | leq | hx | r1 | r2 := _isconv_prog Γ leq t1 π1 h1 t2 π2 h2 hx r1 r2 aux } ;

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

    _isconv (Fallback t2) Γ t1 π1 h1 π2 h2 aux :=
      λ { | leq | hx | r1 | r2 := _isconv_fallback Γ leq t1 π1 h1 t2 π2 h2 r1 r2 hx aux }.


  Equations(noeqns) isconv_full (s : state) (Γ : context)
            (t : term) (π1 : stack) (h1 : wtp Γ t π1)
            (π2 : stack) (h2 : wts Γ s t π2)
    : Ret s Γ t π1 π2 :=
    isconv_full s Γ t π1 h1 π2 h2 hx :=
      Fix_F (R := R Γ)
            (fun pp ⇒ wtp Γ (tm pp) (stk1 pp) → wts Γ (st pp) (tm pp) (stk2 pp)
                    → Ret (st pp) Γ (tm pp) (stk1 pp) (stk2 pp)
                    )
            (fun pp f ⇒ _)
            (x := mkpack Γ s t π1 π2 _)
            _ _ _ _.

  Definition isconv Γ leq t1 π1 h1 t2 π2 h2 hx :=
    let '(exist b _) :=
      isconv_full (Reduction t2) Γ t1 π1 h1 π2 h2 leq hx I I
    in b.

  Theorem isconv_sound :
    ∀ Γ leq t1 π1 h1 t2 π2 h2 hx,
      isconv Γ leq t1 π1 h1 t2 π2 h2 hx →
      conv leq Σ (Γ ,,, stack_context π1) (zipp t1 π1) (zipp t2 π2).

  Definition isconv_term Γ leq t1 (h1 : wellformed Σ Γ t1) t2 (h2 : wellformed Σ Γ t2) :=
    isconv Γ leq t1 ε h1 t2 ε h2 (sq (conv_ctx_refl _ Γ)).

  Theorem isconv_term_sound :
    ∀ Γ leq t1 h1 t2 h2,
      isconv_term Γ leq t1 h1 t2 h2 →
      conv leq Σ Γ t1 t2.

End Conversion.