Theorem: Lean4Lean.VEnv.IsDefEq.strong' (Lean4Lean/Theory/Typing/Strong.lean)

State before:
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
hΓ : CtxStrong env U Γ
H : IsDefEq env U Γ e1 e2 A
⊢ IsDefEqStrong env U Γ e1 e2 A
Tactic:
have hctx {Γ} (H : OnCtx Γ fun Γ A => ∃ u, env.IsDefEqStrong U Γ A A (.sort u)) :
   OnCtx Γ (env.IsType U) := H.mono fun ⟨_, h⟩ => ⟨_, h.defeq⟩
State after:
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
hΓ : CtxStrong env U Γ
H : IsDefEq env U Γ e1 e2 A
hctx : ∀ {Γ : List VExpr}, (OnCtx Γ fun Γ A => ∃ u, IsDefEqStrong env U Γ A A (VExpr.sort u)) → OnCtx Γ (IsType env U)
⊢ IsDefEqStrong env U Γ e1 e2 A

State before:
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
hΓ : CtxStrong env U Γ
H : IsDefEq env U Γ e1 e2 A
hctx : ∀ {Γ : List VExpr}, (OnCtx Γ fun Γ A => ∃ u, IsDefEqStrong env U Γ A A (VExpr.sort u)) → OnCtx Γ (IsType env U)
⊢ IsDefEqStrong env U Γ e1 e2 A
Tactic:
induction H with
| bvar h =>
  let ⟨u, hA⟩ := hΓ.lookup henv h
  exact .bvar h (hA.defeq.sort_r henv (hctx hΓ)) hA
| symm _ ih => exact (ih hΓ).symm
| trans _ _ ih1 ih2 => exact (ih1 hΓ).trans (ih2 hΓ)
| sortDF h1 h2 h3 => exact .sortDF h1 h2 h3
| @constDF _ _ ls₁ ls₂ _ h1 h2 h3 h4 h5 =>
  let ⟨u, h6⟩ := envIH.1 h1
  have H1 := h6.1.instL h2
  have H2 := IsDefEqStrong.defeqDF (u := .succ _) (.inst h2)
    (.symm <| .sortDF (.inst h2) (.inst h3) (VLevel.inst_congr rfl h5)) <| h6.1.instL h3
  exact .constDF h1 h2 h3 h4 h5 (.inst h2) H1 H2 (H1.weak0 henv) (H2.weak0 henv)
| appDF _ _ ih1 ih2 =>
  let ⟨_, h3⟩ := (ih1 hΓ).isType' henv envIH hΓ
  let ⟨⟨u, hA⟩, ⟨v, hB⟩⟩ := h3.forallE_inv' henv envIH hΓ (.inl rfl)
  have hu := hA.defeq.sort_r henv hΓ.defeq
  have hΓ' : CtxStrong env U (_::_) := ⟨hΓ, _, hA⟩
  have hv := hB.defeq.sort_r henv hΓ'.defeq
  exact .appDF hu hv hA hB (ih1 hΓ) (ih2 hΓ) <|
    .instDF (v := v.succ) henv hΓ hu hv hA (.sortDF hv hv rfl) hB (ih2 hΓ)
| lamDF hA _ ih1 ih2 =>
  have hu := hA.sort_r henv hΓ.defeq
  have hΓ' : CtxStrong env U (_::_) := ⟨hΓ, _, (ih1 hΓ).hasType.1⟩
  let ⟨_, hB⟩ := (ih2 hΓ').isType' henv envIH hΓ'
  exact .lamDF hu (hB.defeq.sort_r henv hΓ'.defeq) (ih1 hΓ)
    hB ((ih1 hΓ).defeqDF_l henv hΓ hB) (ih2 hΓ') ((ih1 hΓ).defeqDF_l henv hΓ (ih2 hΓ'))
| forallEDF hA hb ih1 ih2 =>
  have hu := hA.sort_r henv hΓ.defeq
  have hΓ' : CtxStrong env U (_::_) := ⟨hΓ, _, (ih1 hΓ).hasType.1⟩
  exact .forallEDF hu (hb.sort_r henv hΓ'.defeq)
    (ih1 hΓ) (ih2 hΓ') ((ih1 hΓ).defeqDF_l henv hΓ (ih2 hΓ'))
| defeqDF hAB _ ih1 ih2 =>
  exact .defeqDF (hAB.sort_r henv hΓ.defeq) (ih1 hΓ) (ih2 hΓ)
| beta _ _ ih1 ih2 =>
  have he' := ih2 hΓ
  have ⟨_, hA⟩ := he'.isType' henv envIH hΓ
  have hΓ' : CtxStrong env U (_::_) := ⟨hΓ, _, hA⟩
  have he := ih1 hΓ'
  have ⟨_, hB⟩ := he.isType' henv envIH hΓ'
  exact .beta (hA.defeq.sort_r henv hΓ.defeq) (hB.defeq.sort_r henv hΓ'.defeq)
    hA hB he he' (he'.instN henv hΓ .zero hB hΓ) (he'.instN henv hΓ .zero he hΓ)
| eta _ ih =>
  have he := ih hΓ
  let ⟨_, hAB⟩ := he.isType' henv envIH hΓ
  let ⟨⟨u, hA⟩, ⟨v, hB⟩⟩ := hAB.forallE_inv' henv envIH hΓ (.inl rfl)
  have hΓ' : CtxStrong env U (_::_) := ⟨hΓ, _, hA⟩
  exact .eta (hA.defeq.sort_r henv hΓ.defeq) (hB.defeq.sort_r henv hΓ'.defeq)
    hA hB (hB.weakN henv (.succ .one)) he (he.weakN henv .one)
| proofIrrel _ _ _ ih1 ih2 ih3 => exact .proofIrrel (ih1 hΓ) (ih2 hΓ) (ih3 hΓ)
| extra h1 h2 h3 =>
  let ⟨⟨hl, ⟨_, ht⟩, _⟩, hr, _, _⟩ := envIH.2 h1
  exact .extra h1 h2 h3 (.inst h2) (ht.instL h2)
    (hl.instL h2) (hr.instL h2) ((hl.instL h2).weak0 henv) ((hr.instL h2).weak0 henv)
State after:
no goals

State before:
case bvar
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
hctx : ∀ {Γ : List VExpr}, (OnCtx Γ fun Γ A => ∃ u, IsDefEqStrong env U Γ A A (VExpr.sort u)) → OnCtx Γ (IsType env U)
Γ✝ : List VExpr
i✝ : Nat
A✝ : VExpr
h : Lookup Γ✝ i✝ A✝
hΓ : CtxStrong env U Γ✝
⊢ IsDefEqStrong env U Γ✝ (VExpr.bvar i✝) (VExpr.bvar i✝) A✝
Tactic:
let ⟨u, hA⟩ := hΓ.lookup henv h
State after:
case bvar
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
hctx : ∀ {Γ : List VExpr}, (OnCtx Γ fun Γ A => ∃ u, IsDefEqStrong env U Γ A A (VExpr.sort u)) → OnCtx Γ (IsType env U)
Γ✝ : List VExpr
i✝ : Nat
A✝ : VExpr
h : Lookup Γ✝ i✝ A✝
hΓ : CtxStrong env U Γ✝
u : VLevel
hA : IsDefEqStrong env U Γ✝ A✝ A✝ (VExpr.sort u)
⊢ IsDefEqStrong env U Γ✝ (VExpr.bvar i✝) (VExpr.bvar i✝) A✝

State before:
case bvar
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
hctx : ∀ {Γ : List VExpr}, (OnCtx Γ fun Γ A => ∃ u, IsDefEqStrong env U Γ A A (VExpr.sort u)) → OnCtx Γ (IsType env U)
Γ✝ : List VExpr
i✝ : Nat
A✝ : VExpr
h : Lookup Γ✝ i✝ A✝
hΓ : CtxStrong env U Γ✝
u : VLevel
hA : IsDefEqStrong env U Γ✝ A✝ A✝ (VExpr.sort u)
⊢ IsDefEqStrong env U Γ✝ (VExpr.bvar i✝) (VExpr.bvar i✝) A✝
Tactic:
exact .bvar h (hA.defeq.sort_r henv (hctx hΓ)) hA
State after:
no goals

State before:
case symm
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
hctx : ∀ {Γ : List VExpr}, (OnCtx Γ fun Γ A => ∃ u, IsDefEqStrong env U Γ A A (VExpr.sort u)) → OnCtx Γ (IsType env U)
Γ✝ : List VExpr
e✝ e'✝ A✝ : VExpr
a✝ : IsDefEq env U Γ✝ e✝ e'✝ A✝
ih : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ e✝ e'✝ A✝
hΓ : CtxStrong env U Γ✝
⊢ IsDefEqStrong env U Γ✝ e'✝ e✝ A✝
Tactic:
exact (ih hΓ).symm
State after:
no goals

State before:
case trans
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
hctx : ∀ {Γ : List VExpr}, (OnCtx Γ fun Γ A => ∃ u, IsDefEqStrong env U Γ A A (VExpr.sort u)) → OnCtx Γ (IsType env U)
Γ✝ : List VExpr
e₁✝ e₂✝ A✝ e₃✝ : VExpr
a✝¹ : IsDefEq env U Γ✝ e₁✝ e₂✝ A✝
a✝ : IsDefEq env U Γ✝ e₂✝ e₃✝ A✝
ih1 : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ e₁✝ e₂✝ A✝
ih2 : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ e₂✝ e₃✝ A✝
hΓ : CtxStrong env U Γ✝
⊢ IsDefEqStrong env U Γ✝ e₁✝ e₃✝ A✝
Tactic:
exact (ih1 hΓ).trans (ih2 hΓ)
State after:
no goals

State before:
case sortDF
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
hctx : ∀ {Γ : List VExpr}, (OnCtx Γ fun Γ A => ∃ u, IsDefEqStrong env U Γ A A (VExpr.sort u)) → OnCtx Γ (IsType env U)
l✝ l'✝ : VLevel
Γ✝ : List VExpr
h1 : VLevel.WF U l✝
h2 : VLevel.WF U l'✝
h3 : l✝ ≈ l'✝
hΓ : CtxStrong env U Γ✝
⊢ IsDefEqStrong env U Γ✝ (VExpr.sort l✝) (VExpr.sort l'✝) (VExpr.sort (VLevel.succ l✝))
Tactic:
exact .sortDF h1 h2 h3
State after:
no goals

State before:
case constDF
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
hctx : ∀ {Γ : List VExpr}, (OnCtx Γ fun Γ A => ∃ u, IsDefEqStrong env U Γ A A (VExpr.sort u)) → OnCtx Γ (IsType env U)
c✝ : Name
ci✝ : VConstant
ls₁ ls₂ : List VLevel
Γ✝ : List VExpr
h1 : env.constants c✝ = some (some ci✝)
h2 : ∀ (l : VLevel), l ∈ ls₁ → VLevel.WF U l
h3 : ∀ (l : VLevel), l ∈ ls₂ → VLevel.WF U l
h4 : List.length ls₁ = ci✝.uvars
h5 : List.Forall₂ (fun x x_1 => x ≈ x_1) ls₁ ls₂
hΓ : CtxStrong env U Γ✝
⊢ IsDefEqStrong env U Γ✝ (VExpr.const c✝ ls₁) (VExpr.const c✝ ls₂) (VExpr.instL ls₁ ci✝.type)
Tactic:
let ⟨u, h6⟩ := envIH.1 h1
State after:
case constDF
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
hctx : ∀ {Γ : List VExpr}, (OnCtx Γ fun Γ A => ∃ u, IsDefEqStrong env U Γ A A (VExpr.sort u)) → OnCtx Γ (IsType env U)
c✝ : Name
ci✝ : VConstant
ls₁ ls₂ : List VLevel
Γ✝ : List VExpr
h1 : env.constants c✝ = some (some ci✝)
h2 : ∀ (l : VLevel), l ∈ ls₁ → VLevel.WF U l
h3 : ∀ (l : VLevel), l ∈ ls₂ → VLevel.WF U l
h4 : List.length ls₁ = ci✝.uvars
h5 : List.Forall₂ (fun x x_1 => x ≈ x_1) ls₁ ls₂
hΓ : CtxStrong env U Γ✝
u : VLevel
h6 : EnvStrong env ci✝.uvars ci✝.type (VExpr.sort u)
⊢ IsDefEqStrong env U Γ✝ (VExpr.const c✝ ls₁) (VExpr.const c✝ ls₂) (VExpr.instL ls₁ ci✝.type)

State before:
case constDF
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
hctx : ∀ {Γ : List VExpr}, (OnCtx Γ fun Γ A => ∃ u, IsDefEqStrong env U Γ A A (VExpr.sort u)) → OnCtx Γ (IsType env U)
c✝ : Name
ci✝ : VConstant
ls₁ ls₂ : List VLevel
Γ✝ : List VExpr
h1 : env.constants c✝ = some (some ci✝)
h2 : ∀ (l : VLevel), l ∈ ls₁ → VLevel.WF U l
h3 : ∀ (l : VLevel), l ∈ ls₂ → VLevel.WF U l
h4 : List.length ls₁ = ci✝.uvars
h5 : List.Forall₂ (fun x x_1 => x ≈ x_1) ls₁ ls₂
hΓ : CtxStrong env U Γ✝
u : VLevel
h6 : EnvStrong env ci✝.uvars ci✝.type (VExpr.sort u)
⊢ IsDefEqStrong env U Γ✝ (VExpr.const c✝ ls₁) (VExpr.const c✝ ls₂) (VExpr.instL ls₁ ci✝.type)
Tactic:
have H1 := h6.1.instL h2
State after:
case constDF
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
hctx : ∀ {Γ : List VExpr}, (OnCtx Γ fun Γ A => ∃ u, IsDefEqStrong env U Γ A A (VExpr.sort u)) → OnCtx Γ (IsType env U)
c✝ : Name
ci✝ : VConstant
ls₁ ls₂ : List VLevel
Γ✝ : List VExpr
h1 : env.constants c✝ = some (some ci✝)
h2 : ∀ (l : VLevel), l ∈ ls₁ → VLevel.WF U l
h3 : ∀ (l : VLevel), l ∈ ls₂ → VLevel.WF U l
h4 : List.length ls₁ = ci✝.uvars
h5 : List.Forall₂ (fun x x_1 => x ≈ x_1) ls₁ ls₂
hΓ : CtxStrong env U Γ✝
u : VLevel
h6 : EnvStrong env ci✝.uvars ci✝.type (VExpr.sort u)
H1 :
  IsDefEqStrong env U (List.map (VExpr.instL ls₁) []) (VExpr.instL ls₁ ci✝.type) (VExpr.instL ls₁ ci✝.type)
    (VExpr.instL ls₁ (VExpr.sort u))
⊢ IsDefEqStrong env U Γ✝ (VExpr.const c✝ ls₁) (VExpr.const c✝ ls₂) (VExpr.instL ls₁ ci✝.type)

State before:
case constDF
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
hctx : ∀ {Γ : List VExpr}, (OnCtx Γ fun Γ A => ∃ u, IsDefEqStrong env U Γ A A (VExpr.sort u)) → OnCtx Γ (IsType env U)
c✝ : Name
ci✝ : VConstant
ls₁ ls₂ : List VLevel
Γ✝ : List VExpr
h1 : env.constants c✝ = some (some ci✝)
h2 : ∀ (l : VLevel), l ∈ ls₁ → VLevel.WF U l
h3 : ∀ (l : VLevel), l ∈ ls₂ → VLevel.WF U l
h4 : List.length ls₁ = ci✝.uvars
h5 : List.Forall₂ (fun x x_1 => x ≈ x_1) ls₁ ls₂
hΓ : CtxStrong env U Γ✝
u : VLevel
h6 : EnvStrong env ci✝.uvars ci✝.type (VExpr.sort u)
H1 :
  IsDefEqStrong env U (List.map (VExpr.instL ls₁) []) (VExpr.instL ls₁ ci✝.type) (VExpr.instL ls₁ ci✝.type)
    (VExpr.instL ls₁ (VExpr.sort u))
⊢ IsDefEqStrong env U Γ✝ (VExpr.const c✝ ls₁) (VExpr.const c✝ ls₂) (VExpr.instL ls₁ ci✝.type)
Tactic:
have H2 := IsDefEqStrong.defeqDF (u := .succ _) (.inst h2)
  (.symm <| .sortDF (.inst h2) (.inst h3) (VLevel.inst_congr rfl h5)) <| h6.1.instL h3
State after:
case constDF
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
hctx : ∀ {Γ : List VExpr}, (OnCtx Γ fun Γ A => ∃ u, IsDefEqStrong env U Γ A A (VExpr.sort u)) → OnCtx Γ (IsType env U)
c✝ : Name
ci✝ : VConstant
ls₁ ls₂ : List VLevel
Γ✝ : List VExpr
h1 : env.constants c✝ = some (some ci✝)
h2 : ∀ (l : VLevel), l ∈ ls₁ → VLevel.WF U l
h3 : ∀ (l : VLevel), l ∈ ls₂ → VLevel.WF U l
h4 : List.length ls₁ = ci✝.uvars
h5 : List.Forall₂ (fun x x_1 => x ≈ x_1) ls₁ ls₂
hΓ : CtxStrong env U Γ✝
u : VLevel
h6 : EnvStrong env ci✝.uvars ci✝.type (VExpr.sort u)
H1 :
  IsDefEqStrong env U (List.map (VExpr.instL ls₁) []) (VExpr.instL ls₁ ci✝.type) (VExpr.instL ls₁ ci✝.type)
    (VExpr.instL ls₁ (VExpr.sort u))
H2 :
  IsDefEqStrong env U (List.map (VExpr.instL ls₂) []) (VExpr.instL ls₂ ci✝.type) (VExpr.instL ls₂ ci✝.type)
    (VExpr.sort (VLevel.inst ls₁ u))
⊢ IsDefEqStrong env U Γ✝ (VExpr.const c✝ ls₁) (VExpr.const c✝ ls₂) (VExpr.instL ls₁ ci✝.type)

State before:
case constDF
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
hctx : ∀ {Γ : List VExpr}, (OnCtx Γ fun Γ A => ∃ u, IsDefEqStrong env U Γ A A (VExpr.sort u)) → OnCtx Γ (IsType env U)
c✝ : Name
ci✝ : VConstant
ls₁ ls₂ : List VLevel
Γ✝ : List VExpr
h1 : env.constants c✝ = some (some ci✝)
h2 : ∀ (l : VLevel), l ∈ ls₁ → VLevel.WF U l
h3 : ∀ (l : VLevel), l ∈ ls₂ → VLevel.WF U l
h4 : List.length ls₁ = ci✝.uvars
h5 : List.Forall₂ (fun x x_1 => x ≈ x_1) ls₁ ls₂
hΓ : CtxStrong env U Γ✝
u : VLevel
h6 : EnvStrong env ci✝.uvars ci✝.type (VExpr.sort u)
H1 :
  IsDefEqStrong env U (List.map (VExpr.instL ls₁) []) (VExpr.instL ls₁ ci✝.type) (VExpr.instL ls₁ ci✝.type)
    (VExpr.instL ls₁ (VExpr.sort u))
H2 :
  IsDefEqStrong env U (List.map (VExpr.instL ls₂) []) (VExpr.instL ls₂ ci✝.type) (VExpr.instL ls₂ ci✝.type)
    (VExpr.sort (VLevel.inst ls₁ u))
⊢ IsDefEqStrong env U Γ✝ (VExpr.const c✝ ls₁) (VExpr.const c✝ ls₂) (VExpr.instL ls₁ ci✝.type)
Tactic:
exact .constDF h1 h2 h3 h4 h5 (.inst h2) H1 H2 (H1.weak0 henv) (H2.weak0 henv)
State after:
no goals

State before:
case appDF
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
hctx : ∀ {Γ : List VExpr}, (OnCtx Γ fun Γ A => ∃ u, IsDefEqStrong env U Γ A A (VExpr.sort u)) → OnCtx Γ (IsType env U)
Γ✝ : List VExpr
f✝ f'✝ A✝ B✝ a✝² a'✝ : VExpr
a✝¹ : IsDefEq env U Γ✝ f✝ f'✝ (VExpr.forallE A✝ B✝)
a✝ : IsDefEq env U Γ✝ a✝² a'✝ A✝
ih1 : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ f✝ f'✝ (VExpr.forallE A✝ B✝)
ih2 : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ a✝² a'✝ A✝
hΓ : CtxStrong env U Γ✝
⊢ IsDefEqStrong env U Γ✝ (app f✝ a✝²) (app f'✝ a'✝) (inst B✝ a✝²)
Tactic:
let ⟨_, h3⟩ := (ih1 hΓ).isType' henv envIH hΓ
State after:
case appDF
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
hctx : ∀ {Γ : List VExpr}, (OnCtx Γ fun Γ A => ∃ u, IsDefEqStrong env U Γ A A (VExpr.sort u)) → OnCtx Γ (IsType env U)
Γ✝ : List VExpr
f✝ f'✝ A✝ B✝ a✝² a'✝ : VExpr
a✝¹ : IsDefEq env U Γ✝ f✝ f'✝ (VExpr.forallE A✝ B✝)
a✝ : IsDefEq env U Γ✝ a✝² a'✝ A✝
ih1 : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ f✝ f'✝ (VExpr.forallE A✝ B✝)
ih2 : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ a✝² a'✝ A✝
hΓ : CtxStrong env U Γ✝
w✝ : VLevel
h3 : IsDefEqStrong env U Γ✝ (VExpr.forallE A✝ B✝) (VExpr.forallE A✝ B✝) (VExpr.sort w✝)
⊢ IsDefEqStrong env U Γ✝ (app f✝ a✝²) (app f'✝ a'✝) (inst B✝ a✝²)

State before:
case appDF
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
hctx : ∀ {Γ : List VExpr}, (OnCtx Γ fun Γ A => ∃ u, IsDefEqStrong env U Γ A A (VExpr.sort u)) → OnCtx Γ (IsType env U)
Γ✝ : List VExpr
f✝ f'✝ A✝ B✝ a✝² a'✝ : VExpr
a✝¹ : IsDefEq env U Γ✝ f✝ f'✝ (VExpr.forallE A✝ B✝)
a✝ : IsDefEq env U Γ✝ a✝² a'✝ A✝
ih1 : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ f✝ f'✝ (VExpr.forallE A✝ B✝)
ih2 : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ a✝² a'✝ A✝
hΓ : CtxStrong env U Γ✝
w✝ : VLevel
h3 : IsDefEqStrong env U Γ✝ (VExpr.forallE A✝ B✝) (VExpr.forallE A✝ B✝) (VExpr.sort w✝)
⊢ IsDefEqStrong env U Γ✝ (app f✝ a✝²) (app f'✝ a'✝) (inst B✝ a✝²)
Tactic:
let ⟨⟨u, hA⟩, ⟨v, hB⟩⟩ := h3.forallE_inv' henv envIH hΓ (.inl rfl)
State after:
case appDF
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
hctx : ∀ {Γ : List VExpr}, (OnCtx Γ fun Γ A => ∃ u, IsDefEqStrong env U Γ A A (VExpr.sort u)) → OnCtx Γ (IsType env U)
Γ✝ : List VExpr
f✝ f'✝ A✝ B✝ a✝² a'✝ : VExpr
a✝¹ : IsDefEq env U Γ✝ f✝ f'✝ (VExpr.forallE A✝ B✝)
a✝ : IsDefEq env U Γ✝ a✝² a'✝ A✝
ih1 : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ f✝ f'✝ (VExpr.forallE A✝ B✝)
ih2 : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ a✝² a'✝ A✝
hΓ : CtxStrong env U Γ✝
w✝ : VLevel
h3 : IsDefEqStrong env U Γ✝ (VExpr.forallE A✝ B✝) (VExpr.forallE A✝ B✝) (VExpr.sort w✝)
u : VLevel
hA : IsDefEqStrong env U Γ✝ A✝ A✝ (VExpr.sort u)
v : VLevel
hB : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (VExpr.sort v)
⊢ IsDefEqStrong env U Γ✝ (app f✝ a✝²) (app f'✝ a'✝) (inst B✝ a✝²)

State before:
case appDF
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
hctx : ∀ {Γ : List VExpr}, (OnCtx Γ fun Γ A => ∃ u, IsDefEqStrong env U Γ A A (VExpr.sort u)) → OnCtx Γ (IsType env U)
Γ✝ : List VExpr
f✝ f'✝ A✝ B✝ a✝² a'✝ : VExpr
a✝¹ : IsDefEq env U Γ✝ f✝ f'✝ (VExpr.forallE A✝ B✝)
a✝ : IsDefEq env U Γ✝ a✝² a'✝ A✝
ih1 : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ f✝ f'✝ (VExpr.forallE A✝ B✝)
ih2 : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ a✝² a'✝ A✝
hΓ : CtxStrong env U Γ✝
w✝ : VLevel
h3 : IsDefEqStrong env U Γ✝ (VExpr.forallE A✝ B✝) (VExpr.forallE A✝ B✝) (VExpr.sort w✝)
u : VLevel
hA : IsDefEqStrong env U Γ✝ A✝ A✝ (VExpr.sort u)
v : VLevel
hB : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (VExpr.sort v)
⊢ IsDefEqStrong env U Γ✝ (app f✝ a✝²) (app f'✝ a'✝) (inst B✝ a✝²)
Tactic:
have hu := hA.defeq.sort_r henv hΓ.defeq
State after:
case appDF
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
hctx : ∀ {Γ : List VExpr}, (OnCtx Γ fun Γ A => ∃ u, IsDefEqStrong env U Γ A A (VExpr.sort u)) → OnCtx Γ (IsType env U)
Γ✝ : List VExpr
f✝ f'✝ A✝ B✝ a✝² a'✝ : VExpr
a✝¹ : IsDefEq env U Γ✝ f✝ f'✝ (VExpr.forallE A✝ B✝)
a✝ : IsDefEq env U Γ✝ a✝² a'✝ A✝
ih1 : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ f✝ f'✝ (VExpr.forallE A✝ B✝)
ih2 : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ a✝² a'✝ A✝
hΓ : CtxStrong env U Γ✝
w✝ : VLevel
h3 : IsDefEqStrong env U Γ✝ (VExpr.forallE A✝ B✝) (VExpr.forallE A✝ B✝) (VExpr.sort w✝)
u : VLevel
hA : IsDefEqStrong env U Γ✝ A✝ A✝ (VExpr.sort u)
v : VLevel
hB : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (VExpr.sort v)
hu : VLevel.WF U u
⊢ IsDefEqStrong env U Γ✝ (app f✝ a✝²) (app f'✝ a'✝) (inst B✝ a✝²)

State before:
case appDF
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
hctx : ∀ {Γ : List VExpr}, (OnCtx Γ fun Γ A => ∃ u, IsDefEqStrong env U Γ A A (VExpr.sort u)) → OnCtx Γ (IsType env U)
Γ✝ : List VExpr
f✝ f'✝ A✝ B✝ a✝² a'✝ : VExpr
a✝¹ : IsDefEq env U Γ✝ f✝ f'✝ (VExpr.forallE A✝ B✝)
a✝ : IsDefEq env U Γ✝ a✝² a'✝ A✝
ih1 : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ f✝ f'✝ (VExpr.forallE A✝ B✝)
ih2 : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ a✝² a'✝ A✝
hΓ : CtxStrong env U Γ✝
w✝ : VLevel
h3 : IsDefEqStrong env U Γ✝ (VExpr.forallE A✝ B✝) (VExpr.forallE A✝ B✝) (VExpr.sort w✝)
u : VLevel
hA : IsDefEqStrong env U Γ✝ A✝ A✝ (VExpr.sort u)
v : VLevel
hB : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (VExpr.sort v)
hu : VLevel.WF U u
⊢ IsDefEqStrong env U Γ✝ (app f✝ a✝²) (app f'✝ a'✝) (inst B✝ a✝²)
Tactic:
have hΓ' : CtxStrong env U (_::_) := ⟨hΓ, _, hA⟩
State after:
case appDF
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
hctx : ∀ {Γ : List VExpr}, (OnCtx Γ fun Γ A => ∃ u, IsDefEqStrong env U Γ A A (VExpr.sort u)) → OnCtx Γ (IsType env U)
Γ✝ : List VExpr
f✝ f'✝ A✝ B✝ a✝² a'✝ : VExpr
a✝¹ : IsDefEq env U Γ✝ f✝ f'✝ (VExpr.forallE A✝ B✝)
a✝ : IsDefEq env U Γ✝ a✝² a'✝ A✝
ih1 : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ f✝ f'✝ (VExpr.forallE A✝ B✝)
ih2 : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ a✝² a'✝ A✝
hΓ : CtxStrong env U Γ✝
w✝ : VLevel
h3 : IsDefEqStrong env U Γ✝ (VExpr.forallE A✝ B✝) (VExpr.forallE A✝ B✝) (VExpr.sort w✝)
u : VLevel
hA : IsDefEqStrong env U Γ✝ A✝ A✝ (VExpr.sort u)
v : VLevel
hB : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (VExpr.sort v)
hu : VLevel.WF U u
hΓ' : CtxStrong env U (A✝ :: Γ✝)
⊢ IsDefEqStrong env U Γ✝ (app f✝ a✝²) (app f'✝ a'✝) (inst B✝ a✝²)

State before:
case appDF
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
hctx : ∀ {Γ : List VExpr}, (OnCtx Γ fun Γ A => ∃ u, IsDefEqStrong env U Γ A A (VExpr.sort u)) → OnCtx Γ (IsType env U)
Γ✝ : List VExpr
f✝ f'✝ A✝ B✝ a✝² a'✝ : VExpr
a✝¹ : IsDefEq env U Γ✝ f✝ f'✝ (VExpr.forallE A✝ B✝)
a✝ : IsDefEq env U Γ✝ a✝² a'✝ A✝
ih1 : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ f✝ f'✝ (VExpr.forallE A✝ B✝)
ih2 : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ a✝² a'✝ A✝
hΓ : CtxStrong env U Γ✝
w✝ : VLevel
h3 : IsDefEqStrong env U Γ✝ (VExpr.forallE A✝ B✝) (VExpr.forallE A✝ B✝) (VExpr.sort w✝)
u : VLevel
hA : IsDefEqStrong env U Γ✝ A✝ A✝ (VExpr.sort u)
v : VLevel
hB : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (VExpr.sort v)
hu : VLevel.WF U u
hΓ' : CtxStrong env U (A✝ :: Γ✝)
⊢ IsDefEqStrong env U Γ✝ (app f✝ a✝²) (app f'✝ a'✝) (inst B✝ a✝²)
Tactic:
have hv := hB.defeq.sort_r henv hΓ'.defeq
State after:
case appDF
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
hctx : ∀ {Γ : List VExpr}, (OnCtx Γ fun Γ A => ∃ u, IsDefEqStrong env U Γ A A (VExpr.sort u)) → OnCtx Γ (IsType env U)
Γ✝ : List VExpr
f✝ f'✝ A✝ B✝ a✝² a'✝ : VExpr
a✝¹ : IsDefEq env U Γ✝ f✝ f'✝ (VExpr.forallE A✝ B✝)
a✝ : IsDefEq env U Γ✝ a✝² a'✝ A✝
ih1 : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ f✝ f'✝ (VExpr.forallE A✝ B✝)
ih2 : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ a✝² a'✝ A✝
hΓ : CtxStrong env U Γ✝
w✝ : VLevel
h3 : IsDefEqStrong env U Γ✝ (VExpr.forallE A✝ B✝) (VExpr.forallE A✝ B✝) (VExpr.sort w✝)
u : VLevel
hA : IsDefEqStrong env U Γ✝ A✝ A✝ (VExpr.sort u)
v : VLevel
hB : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (VExpr.sort v)
hu : VLevel.WF U u
hΓ' : CtxStrong env U (A✝ :: Γ✝)
hv : VLevel.WF U v
⊢ IsDefEqStrong env U Γ✝ (app f✝ a✝²) (app f'✝ a'✝) (inst B✝ a✝²)

State before:
case appDF
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
hctx : ∀ {Γ : List VExpr}, (OnCtx Γ fun Γ A => ∃ u, IsDefEqStrong env U Γ A A (VExpr.sort u)) → OnCtx Γ (IsType env U)
Γ✝ : List VExpr
f✝ f'✝ A✝ B✝ a✝² a'✝ : VExpr
a✝¹ : IsDefEq env U Γ✝ f✝ f'✝ (VExpr.forallE A✝ B✝)
a✝ : IsDefEq env U Γ✝ a✝² a'✝ A✝
ih1 : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ f✝ f'✝ (VExpr.forallE A✝ B✝)
ih2 : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ a✝² a'✝ A✝
hΓ : CtxStrong env U Γ✝
w✝ : VLevel
h3 : IsDefEqStrong env U Γ✝ (VExpr.forallE A✝ B✝) (VExpr.forallE A✝ B✝) (VExpr.sort w✝)
u : VLevel
hA : IsDefEqStrong env U Γ✝ A✝ A✝ (VExpr.sort u)
v : VLevel
hB : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (VExpr.sort v)
hu : VLevel.WF U u
hΓ' : CtxStrong env U (A✝ :: Γ✝)
hv : VLevel.WF U v
⊢ IsDefEqStrong env U Γ✝ (app f✝ a✝²) (app f'✝ a'✝) (inst B✝ a✝²)
Tactic:
exact .appDF hu hv hA hB (ih1 hΓ) (ih2 hΓ) <|
  .instDF (v := v.succ) henv hΓ hu hv hA (.sortDF hv hv rfl) hB (ih2 hΓ)
State after:
no goals

State before:
case lamDF
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
hctx : ∀ {Γ : List VExpr}, (OnCtx Γ fun Γ A => ∃ u, IsDefEqStrong env U Γ A A (VExpr.sort u)) → OnCtx Γ (IsType env U)
Γ✝ : List VExpr
A✝ A'✝ : VExpr
u✝ : VLevel
body✝ body'✝ B✝ : VExpr
hA : IsDefEq env U Γ✝ A✝ A'✝ (VExpr.sort u✝)
a✝ : IsDefEq env U (A✝ :: Γ✝) body✝ body'✝ B✝
ih1 : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ A✝ A'✝ (VExpr.sort u✝)
ih2 : CtxStrong env U (A✝ :: Γ✝) → IsDefEqStrong env U (A✝ :: Γ✝) body✝ body'✝ B✝
hΓ : CtxStrong env U Γ✝
⊢ IsDefEqStrong env U Γ✝ (lam A✝ body✝) (lam A'✝ body'✝) (VExpr.forallE A✝ B✝)
Tactic:
have hu := hA.sort_r henv hΓ.defeq
State after:
case lamDF
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
hctx : ∀ {Γ : List VExpr}, (OnCtx Γ fun Γ A => ∃ u, IsDefEqStrong env U Γ A A (VExpr.sort u)) → OnCtx Γ (IsType env U)
Γ✝ : List VExpr
A✝ A'✝ : VExpr
u✝ : VLevel
body✝ body'✝ B✝ : VExpr
hA : IsDefEq env U Γ✝ A✝ A'✝ (VExpr.sort u✝)
a✝ : IsDefEq env U (A✝ :: Γ✝) body✝ body'✝ B✝
ih1 : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ A✝ A'✝ (VExpr.sort u✝)
ih2 : CtxStrong env U (A✝ :: Γ✝) → IsDefEqStrong env U (A✝ :: Γ✝) body✝ body'✝ B✝
hΓ : CtxStrong env U Γ✝
hu : VLevel.WF U u✝
⊢ IsDefEqStrong env U Γ✝ (lam A✝ body✝) (lam A'✝ body'✝) (VExpr.forallE A✝ B✝)

State before:
case lamDF
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
hctx : ∀ {Γ : List VExpr}, (OnCtx Γ fun Γ A => ∃ u, IsDefEqStrong env U Γ A A (VExpr.sort u)) → OnCtx Γ (IsType env U)
Γ✝ : List VExpr
A✝ A'✝ : VExpr
u✝ : VLevel
body✝ body'✝ B✝ : VExpr
hA : IsDefEq env U Γ✝ A✝ A'✝ (VExpr.sort u✝)
a✝ : IsDefEq env U (A✝ :: Γ✝) body✝ body'✝ B✝
ih1 : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ A✝ A'✝ (VExpr.sort u✝)
ih2 : CtxStrong env U (A✝ :: Γ✝) → IsDefEqStrong env U (A✝ :: Γ✝) body✝ body'✝ B✝
hΓ : CtxStrong env U Γ✝
hu : VLevel.WF U u✝
⊢ IsDefEqStrong env U Γ✝ (lam A✝ body✝) (lam A'✝ body'✝) (VExpr.forallE A✝ B✝)
Tactic:
have hΓ' : CtxStrong env U (_::_) := ⟨hΓ, _, (ih1 hΓ).hasType.1⟩
State after:
case lamDF
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
hctx : ∀ {Γ : List VExpr}, (OnCtx Γ fun Γ A => ∃ u, IsDefEqStrong env U Γ A A (VExpr.sort u)) → OnCtx Γ (IsType env U)
Γ✝ : List VExpr
A✝ A'✝ : VExpr
u✝ : VLevel
body✝ body'✝ B✝ : VExpr
hA : IsDefEq env U Γ✝ A✝ A'✝ (VExpr.sort u✝)
a✝ : IsDefEq env U (A✝ :: Γ✝) body✝ body'✝ B✝
ih1 : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ A✝ A'✝ (VExpr.sort u✝)
ih2 : CtxStrong env U (A✝ :: Γ✝) → IsDefEqStrong env U (A✝ :: Γ✝) body✝ body'✝ B✝
hΓ : CtxStrong env U Γ✝
hu : VLevel.WF U u✝
hΓ' : CtxStrong env U (A✝ :: Γ✝)
⊢ IsDefEqStrong env U Γ✝ (lam A✝ body✝) (lam A'✝ body'✝) (VExpr.forallE A✝ B✝)

State before:
case lamDF
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
hctx : ∀ {Γ : List VExpr}, (OnCtx Γ fun Γ A => ∃ u, IsDefEqStrong env U Γ A A (VExpr.sort u)) → OnCtx Γ (IsType env U)
Γ✝ : List VExpr
A✝ A'✝ : VExpr
u✝ : VLevel
body✝ body'✝ B✝ : VExpr
hA : IsDefEq env U Γ✝ A✝ A'✝ (VExpr.sort u✝)
a✝ : IsDefEq env U (A✝ :: Γ✝) body✝ body'✝ B✝
ih1 : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ A✝ A'✝ (VExpr.sort u✝)
ih2 : CtxStrong env U (A✝ :: Γ✝) → IsDefEqStrong env U (A✝ :: Γ✝) body✝ body'✝ B✝
hΓ : CtxStrong env U Γ✝
hu : VLevel.WF U u✝
hΓ' : CtxStrong env U (A✝ :: Γ✝)
⊢ IsDefEqStrong env U Γ✝ (lam A✝ body✝) (lam A'✝ body'✝) (VExpr.forallE A✝ B✝)
Tactic:
let ⟨_, hB⟩ := (ih2 hΓ').isType' henv envIH hΓ'
State after:
case lamDF
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
hctx : ∀ {Γ : List VExpr}, (OnCtx Γ fun Γ A => ∃ u, IsDefEqStrong env U Γ A A (VExpr.sort u)) → OnCtx Γ (IsType env U)
Γ✝ : List VExpr
A✝ A'✝ : VExpr
u✝ : VLevel
body✝ body'✝ B✝ : VExpr
hA : IsDefEq env U Γ✝ A✝ A'✝ (VExpr.sort u✝)
a✝ : IsDefEq env U (A✝ :: Γ✝) body✝ body'✝ B✝
ih1 : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ A✝ A'✝ (VExpr.sort u✝)
ih2 : CtxStrong env U (A✝ :: Γ✝) → IsDefEqStrong env U (A✝ :: Γ✝) body✝ body'✝ B✝
hΓ : CtxStrong env U Γ✝
hu : VLevel.WF U u✝
hΓ' : CtxStrong env U (A✝ :: Γ✝)
w✝ : VLevel
hB : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (VExpr.sort w✝)
⊢ IsDefEqStrong env U Γ✝ (lam A✝ body✝) (lam A'✝ body'✝) (VExpr.forallE A✝ B✝)

State before:
case lamDF
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
hctx : ∀ {Γ : List VExpr}, (OnCtx Γ fun Γ A => ∃ u, IsDefEqStrong env U Γ A A (VExpr.sort u)) → OnCtx Γ (IsType env U)
Γ✝ : List VExpr
A✝ A'✝ : VExpr
u✝ : VLevel
body✝ body'✝ B✝ : VExpr
hA : IsDefEq env U Γ✝ A✝ A'✝ (VExpr.sort u✝)
a✝ : IsDefEq env U (A✝ :: Γ✝) body✝ body'✝ B✝
ih1 : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ A✝ A'✝ (VExpr.sort u✝)
ih2 : CtxStrong env U (A✝ :: Γ✝) → IsDefEqStrong env U (A✝ :: Γ✝) body✝ body'✝ B✝
hΓ : CtxStrong env U Γ✝
hu : VLevel.WF U u✝
hΓ' : CtxStrong env U (A✝ :: Γ✝)
w✝ : VLevel
hB : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (VExpr.sort w✝)
⊢ IsDefEqStrong env U Γ✝ (lam A✝ body✝) (lam A'✝ body'✝) (VExpr.forallE A✝ B✝)
Tactic:
exact .lamDF hu (hB.defeq.sort_r henv hΓ'.defeq) (ih1 hΓ)
  hB ((ih1 hΓ).defeqDF_l henv hΓ hB) (ih2 hΓ') ((ih1 hΓ).defeqDF_l henv hΓ (ih2 hΓ'))
State after:
no goals

State before:
case forallEDF
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
hctx : ∀ {Γ : List VExpr}, (OnCtx Γ fun Γ A => ∃ u, IsDefEqStrong env U Γ A A (VExpr.sort u)) → OnCtx Γ (IsType env U)
Γ✝ : List VExpr
A✝ A'✝ : VExpr
u✝ : VLevel
body✝ body'✝ : VExpr
v✝ : VLevel
hA : IsDefEq env U Γ✝ A✝ A'✝ (VExpr.sort u✝)
hb : IsDefEq env U (A✝ :: Γ✝) body✝ body'✝ (VExpr.sort v✝)
ih1 : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ A✝ A'✝ (VExpr.sort u✝)
ih2 : CtxStrong env U (A✝ :: Γ✝) → IsDefEqStrong env U (A✝ :: Γ✝) body✝ body'✝ (VExpr.sort v✝)
hΓ : CtxStrong env U Γ✝
⊢ IsDefEqStrong env U Γ✝ (VExpr.forallE A✝ body✝) (VExpr.forallE A'✝ body'✝) (VExpr.sort (VLevel.imax u✝ v✝))
Tactic:
have hu := hA.sort_r henv hΓ.defeq
State after:
case forallEDF
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
hctx : ∀ {Γ : List VExpr}, (OnCtx Γ fun Γ A => ∃ u, IsDefEqStrong env U Γ A A (VExpr.sort u)) → OnCtx Γ (IsType env U)
Γ✝ : List VExpr
A✝ A'✝ : VExpr
u✝ : VLevel
body✝ body'✝ : VExpr
v✝ : VLevel
hA : IsDefEq env U Γ✝ A✝ A'✝ (VExpr.sort u✝)
hb : IsDefEq env U (A✝ :: Γ✝) body✝ body'✝ (VExpr.sort v✝)
ih1 : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ A✝ A'✝ (VExpr.sort u✝)
ih2 : CtxStrong env U (A✝ :: Γ✝) → IsDefEqStrong env U (A✝ :: Γ✝) body✝ body'✝ (VExpr.sort v✝)
hΓ : CtxStrong env U Γ✝
hu : VLevel.WF U u✝
⊢ IsDefEqStrong env U Γ✝ (VExpr.forallE A✝ body✝) (VExpr.forallE A'✝ body'✝) (VExpr.sort (VLevel.imax u✝ v✝))

State before:
case forallEDF
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
hctx : ∀ {Γ : List VExpr}, (OnCtx Γ fun Γ A => ∃ u, IsDefEqStrong env U Γ A A (VExpr.sort u)) → OnCtx Γ (IsType env U)
Γ✝ : List VExpr
A✝ A'✝ : VExpr
u✝ : VLevel
body✝ body'✝ : VExpr
v✝ : VLevel
hA : IsDefEq env U Γ✝ A✝ A'✝ (VExpr.sort u✝)
hb : IsDefEq env U (A✝ :: Γ✝) body✝ body'✝ (VExpr.sort v✝)
ih1 : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ A✝ A'✝ (VExpr.sort u✝)
ih2 : CtxStrong env U (A✝ :: Γ✝) → IsDefEqStrong env U (A✝ :: Γ✝) body✝ body'✝ (VExpr.sort v✝)
hΓ : CtxStrong env U Γ✝
hu : VLevel.WF U u✝
⊢ IsDefEqStrong env U Γ✝ (VExpr.forallE A✝ body✝) (VExpr.forallE A'✝ body'✝) (VExpr.sort (VLevel.imax u✝ v✝))
Tactic:
have hΓ' : CtxStrong env U (_::_) := ⟨hΓ, _, (ih1 hΓ).hasType.1⟩
State after:
case forallEDF
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
hctx : ∀ {Γ : List VExpr}, (OnCtx Γ fun Γ A => ∃ u, IsDefEqStrong env U Γ A A (VExpr.sort u)) → OnCtx Γ (IsType env U)
Γ✝ : List VExpr
A✝ A'✝ : VExpr
u✝ : VLevel
body✝ body'✝ : VExpr
v✝ : VLevel
hA : IsDefEq env U Γ✝ A✝ A'✝ (VExpr.sort u✝)
hb : IsDefEq env U (A✝ :: Γ✝) body✝ body'✝ (VExpr.sort v✝)
ih1 : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ A✝ A'✝ (VExpr.sort u✝)
ih2 : CtxStrong env U (A✝ :: Γ✝) → IsDefEqStrong env U (A✝ :: Γ✝) body✝ body'✝ (VExpr.sort v✝)
hΓ : CtxStrong env U Γ✝
hu : VLevel.WF U u✝
hΓ' : CtxStrong env U (A✝ :: Γ✝)
⊢ IsDefEqStrong env U Γ✝ (VExpr.forallE A✝ body✝) (VExpr.forallE A'✝ body'✝) (VExpr.sort (VLevel.imax u✝ v✝))

State before:
case forallEDF
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
hctx : ∀ {Γ : List VExpr}, (OnCtx Γ fun Γ A => ∃ u, IsDefEqStrong env U Γ A A (VExpr.sort u)) → OnCtx Γ (IsType env U)
Γ✝ : List VExpr
A✝ A'✝ : VExpr
u✝ : VLevel
body✝ body'✝ : VExpr
v✝ : VLevel
hA : IsDefEq env U Γ✝ A✝ A'✝ (VExpr.sort u✝)
hb : IsDefEq env U (A✝ :: Γ✝) body✝ body'✝ (VExpr.sort v✝)
ih1 : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ A✝ A'✝ (VExpr.sort u✝)
ih2 : CtxStrong env U (A✝ :: Γ✝) → IsDefEqStrong env U (A✝ :: Γ✝) body✝ body'✝ (VExpr.sort v✝)
hΓ : CtxStrong env U Γ✝
hu : VLevel.WF U u✝
hΓ' : CtxStrong env U (A✝ :: Γ✝)
⊢ IsDefEqStrong env U Γ✝ (VExpr.forallE A✝ body✝) (VExpr.forallE A'✝ body'✝) (VExpr.sort (VLevel.imax u✝ v✝))
Tactic:
exact .forallEDF hu (hb.sort_r henv hΓ'.defeq)
  (ih1 hΓ) (ih2 hΓ') ((ih1 hΓ).defeqDF_l henv hΓ (ih2 hΓ'))
State after:
no goals

State before:
case defeqDF
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
hctx : ∀ {Γ : List VExpr}, (OnCtx Γ fun Γ A => ∃ u, IsDefEqStrong env U Γ A A (VExpr.sort u)) → OnCtx Γ (IsType env U)
Γ✝ : List VExpr
A✝ B✝ : VExpr
u✝ : VLevel
e1✝ e2✝ : VExpr
hAB : IsDefEq env U Γ✝ A✝ B✝ (VExpr.sort u✝)
a✝ : IsDefEq env U Γ✝ e1✝ e2✝ A✝
ih1 : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ A✝ B✝ (VExpr.sort u✝)
ih2 : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ e1✝ e2✝ A✝
hΓ : CtxStrong env U Γ✝
⊢ IsDefEqStrong env U Γ✝ e1✝ e2✝ B✝
Tactic:
exact .defeqDF (hAB.sort_r henv hΓ.defeq) (ih1 hΓ) (ih2 hΓ)
State after:
no goals

State before:
case beta
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
hctx : ∀ {Γ : List VExpr}, (OnCtx Γ fun Γ A => ∃ u, IsDefEqStrong env U Γ A A (VExpr.sort u)) → OnCtx Γ (IsType env U)
A✝ : VExpr
Γ✝ : List VExpr
e✝ B✝ e'✝ : VExpr
a✝¹ : IsDefEq env U (A✝ :: Γ✝) e✝ e✝ B✝
a✝ : IsDefEq env U Γ✝ e'✝ e'✝ A✝
ih1 : CtxStrong env U (A✝ :: Γ✝) → IsDefEqStrong env U (A✝ :: Γ✝) e✝ e✝ B✝
ih2 : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ e'✝ e'✝ A✝
hΓ : CtxStrong env U Γ✝
⊢ IsDefEqStrong env U Γ✝ (app (lam A✝ e✝) e'✝) (inst e✝ e'✝) (inst B✝ e'✝)
Tactic:
have he' := ih2 hΓ
State after:
case beta
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
hctx : ∀ {Γ : List VExpr}, (OnCtx Γ fun Γ A => ∃ u, IsDefEqStrong env U Γ A A (VExpr.sort u)) → OnCtx Γ (IsType env U)
A✝ : VExpr
Γ✝ : List VExpr
e✝ B✝ e'✝ : VExpr
a✝¹ : IsDefEq env U (A✝ :: Γ✝) e✝ e✝ B✝
a✝ : IsDefEq env U Γ✝ e'✝ e'✝ A✝
ih1 : CtxStrong env U (A✝ :: Γ✝) → IsDefEqStrong env U (A✝ :: Γ✝) e✝ e✝ B✝
ih2 : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ e'✝ e'✝ A✝
hΓ : CtxStrong env U Γ✝
he' : IsDefEqStrong env U Γ✝ e'✝ e'✝ A✝
⊢ IsDefEqStrong env U Γ✝ (app (lam A✝ e✝) e'✝) (inst e✝ e'✝) (inst B✝ e'✝)

State before:
case beta
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
hctx : ∀ {Γ : List VExpr}, (OnCtx Γ fun Γ A => ∃ u, IsDefEqStrong env U Γ A A (VExpr.sort u)) → OnCtx Γ (IsType env U)
A✝ : VExpr
Γ✝ : List VExpr
e✝ B✝ e'✝ : VExpr
a✝¹ : IsDefEq env U (A✝ :: Γ✝) e✝ e✝ B✝
a✝ : IsDefEq env U Γ✝ e'✝ e'✝ A✝
ih1 : CtxStrong env U (A✝ :: Γ✝) → IsDefEqStrong env U (A✝ :: Γ✝) e✝ e✝ B✝
ih2 : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ e'✝ e'✝ A✝
hΓ : CtxStrong env U Γ✝
he' : IsDefEqStrong env U Γ✝ e'✝ e'✝ A✝
⊢ IsDefEqStrong env U Γ✝ (app (lam A✝ e✝) e'✝) (inst e✝ e'✝) (inst B✝ e'✝)
Tactic:
have ⟨_, hA⟩ := he'.isType' henv envIH hΓ
State after:
case beta
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
hctx : ∀ {Γ : List VExpr}, (OnCtx Γ fun Γ A => ∃ u, IsDefEqStrong env U Γ A A (VExpr.sort u)) → OnCtx Γ (IsType env U)
A✝ : VExpr
Γ✝ : List VExpr
e✝ B✝ e'✝ : VExpr
a✝¹ : IsDefEq env U (A✝ :: Γ✝) e✝ e✝ B✝
a✝ : IsDefEq env U Γ✝ e'✝ e'✝ A✝
ih1 : CtxStrong env U (A✝ :: Γ✝) → IsDefEqStrong env U (A✝ :: Γ✝) e✝ e✝ B✝
ih2 : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ e'✝ e'✝ A✝
hΓ : CtxStrong env U Γ✝
he' : IsDefEqStrong env U Γ✝ e'✝ e'✝ A✝
w✝ : VLevel
hA : IsDefEqStrong env U Γ✝ A✝ A✝ (VExpr.sort w✝)
⊢ IsDefEqStrong env U Γ✝ (app (lam A✝ e✝) e'✝) (inst e✝ e'✝) (inst B✝ e'✝)

State before:
case beta
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
hctx : ∀ {Γ : List VExpr}, (OnCtx Γ fun Γ A => ∃ u, IsDefEqStrong env U Γ A A (VExpr.sort u)) → OnCtx Γ (IsType env U)
A✝ : VExpr
Γ✝ : List VExpr
e✝ B✝ e'✝ : VExpr
a✝¹ : IsDefEq env U (A✝ :: Γ✝) e✝ e✝ B✝
a✝ : IsDefEq env U Γ✝ e'✝ e'✝ A✝
ih1 : CtxStrong env U (A✝ :: Γ✝) → IsDefEqStrong env U (A✝ :: Γ✝) e✝ e✝ B✝
ih2 : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ e'✝ e'✝ A✝
hΓ : CtxStrong env U Γ✝
he' : IsDefEqStrong env U Γ✝ e'✝ e'✝ A✝
w✝ : VLevel
hA : IsDefEqStrong env U Γ✝ A✝ A✝ (VExpr.sort w✝)
⊢ IsDefEqStrong env U Γ✝ (app (lam A✝ e✝) e'✝) (inst e✝ e'✝) (inst B✝ e'✝)
Tactic:
have hΓ' : CtxStrong env U (_::_) := ⟨hΓ, _, hA⟩
State after:
case beta
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
hctx : ∀ {Γ : List VExpr}, (OnCtx Γ fun Γ A => ∃ u, IsDefEqStrong env U Γ A A (VExpr.sort u)) → OnCtx Γ (IsType env U)
A✝ : VExpr
Γ✝ : List VExpr
e✝ B✝ e'✝ : VExpr
a✝¹ : IsDefEq env U (A✝ :: Γ✝) e✝ e✝ B✝
a✝ : IsDefEq env U Γ✝ e'✝ e'✝ A✝
ih1 : CtxStrong env U (A✝ :: Γ✝) → IsDefEqStrong env U (A✝ :: Γ✝) e✝ e✝ B✝
ih2 : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ e'✝ e'✝ A✝
hΓ : CtxStrong env U Γ✝
he' : IsDefEqStrong env U Γ✝ e'✝ e'✝ A✝
w✝ : VLevel
hA : IsDefEqStrong env U Γ✝ A✝ A✝ (VExpr.sort w✝)
hΓ' : CtxStrong env U (A✝ :: Γ✝)
⊢ IsDefEqStrong env U Γ✝ (app (lam A✝ e✝) e'✝) (inst e✝ e'✝) (inst B✝ e'✝)

State before:
case beta
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
hctx : ∀ {Γ : List VExpr}, (OnCtx Γ fun Γ A => ∃ u, IsDefEqStrong env U Γ A A (VExpr.sort u)) → OnCtx Γ (IsType env U)
A✝ : VExpr
Γ✝ : List VExpr
e✝ B✝ e'✝ : VExpr
a✝¹ : IsDefEq env U (A✝ :: Γ✝) e✝ e✝ B✝
a✝ : IsDefEq env U Γ✝ e'✝ e'✝ A✝
ih1 : CtxStrong env U (A✝ :: Γ✝) → IsDefEqStrong env U (A✝ :: Γ✝) e✝ e✝ B✝
ih2 : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ e'✝ e'✝ A✝
hΓ : CtxStrong env U Γ✝
he' : IsDefEqStrong env U Γ✝ e'✝ e'✝ A✝
w✝ : VLevel
hA : IsDefEqStrong env U Γ✝ A✝ A✝ (VExpr.sort w✝)
hΓ' : CtxStrong env U (A✝ :: Γ✝)
⊢ IsDefEqStrong env U Γ✝ (app (lam A✝ e✝) e'✝) (inst e✝ e'✝) (inst B✝ e'✝)
Tactic:
have he := ih1 hΓ'
State after:
case beta
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
hctx : ∀ {Γ : List VExpr}, (OnCtx Γ fun Γ A => ∃ u, IsDefEqStrong env U Γ A A (VExpr.sort u)) → OnCtx Γ (IsType env U)
A✝ : VExpr
Γ✝ : List VExpr
e✝ B✝ e'✝ : VExpr
a✝¹ : IsDefEq env U (A✝ :: Γ✝) e✝ e✝ B✝
a✝ : IsDefEq env U Γ✝ e'✝ e'✝ A✝
ih1 : CtxStrong env U (A✝ :: Γ✝) → IsDefEqStrong env U (A✝ :: Γ✝) e✝ e✝ B✝
ih2 : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ e'✝ e'✝ A✝
hΓ : CtxStrong env U Γ✝
he' : IsDefEqStrong env U Γ✝ e'✝ e'✝ A✝
w✝ : VLevel
hA : IsDefEqStrong env U Γ✝ A✝ A✝ (VExpr.sort w✝)
hΓ' : CtxStrong env U (A✝ :: Γ✝)
he : IsDefEqStrong env U (A✝ :: Γ✝) e✝ e✝ B✝
⊢ IsDefEqStrong env U Γ✝ (app (lam A✝ e✝) e'✝) (inst e✝ e'✝) (inst B✝ e'✝)

State before:
case beta
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
hctx : ∀ {Γ : List VExpr}, (OnCtx Γ fun Γ A => ∃ u, IsDefEqStrong env U Γ A A (VExpr.sort u)) → OnCtx Γ (IsType env U)
A✝ : VExpr
Γ✝ : List VExpr
e✝ B✝ e'✝ : VExpr
a✝¹ : IsDefEq env U (A✝ :: Γ✝) e✝ e✝ B✝
a✝ : IsDefEq env U Γ✝ e'✝ e'✝ A✝
ih1 : CtxStrong env U (A✝ :: Γ✝) → IsDefEqStrong env U (A✝ :: Γ✝) e✝ e✝ B✝
ih2 : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ e'✝ e'✝ A✝
hΓ : CtxStrong env U Γ✝
he' : IsDefEqStrong env U Γ✝ e'✝ e'✝ A✝
w✝ : VLevel
hA : IsDefEqStrong env U Γ✝ A✝ A✝ (VExpr.sort w✝)
hΓ' : CtxStrong env U (A✝ :: Γ✝)
he : IsDefEqStrong env U (A✝ :: Γ✝) e✝ e✝ B✝
⊢ IsDefEqStrong env U Γ✝ (app (lam A✝ e✝) e'✝) (inst e✝ e'✝) (inst B✝ e'✝)
Tactic:
have ⟨_, hB⟩ := he.isType' henv envIH hΓ'
State after:
case beta
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
hctx : ∀ {Γ : List VExpr}, (OnCtx Γ fun Γ A => ∃ u, IsDefEqStrong env U Γ A A (VExpr.sort u)) → OnCtx Γ (IsType env U)
A✝ : VExpr
Γ✝ : List VExpr
e✝ B✝ e'✝ : VExpr
a✝¹ : IsDefEq env U (A✝ :: Γ✝) e✝ e✝ B✝
a✝ : IsDefEq env U Γ✝ e'✝ e'✝ A✝
ih1 : CtxStrong env U (A✝ :: Γ✝) → IsDefEqStrong env U (A✝ :: Γ✝) e✝ e✝ B✝
ih2 : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ e'✝ e'✝ A✝
hΓ : CtxStrong env U Γ✝
he' : IsDefEqStrong env U Γ✝ e'✝ e'✝ A✝
w✝¹ : VLevel
hA : IsDefEqStrong env U Γ✝ A✝ A✝ (VExpr.sort w✝¹)
hΓ' : CtxStrong env U (A✝ :: Γ✝)
he : IsDefEqStrong env U (A✝ :: Γ✝) e✝ e✝ B✝
w✝ : VLevel
hB : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (VExpr.sort w✝)
⊢ IsDefEqStrong env U Γ✝ (app (lam A✝ e✝) e'✝) (inst e✝ e'✝) (inst B✝ e'✝)

State before:
case beta
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
hctx : ∀ {Γ : List VExpr}, (OnCtx Γ fun Γ A => ∃ u, IsDefEqStrong env U Γ A A (VExpr.sort u)) → OnCtx Γ (IsType env U)
A✝ : VExpr
Γ✝ : List VExpr
e✝ B✝ e'✝ : VExpr
a✝¹ : IsDefEq env U (A✝ :: Γ✝) e✝ e✝ B✝
a✝ : IsDefEq env U Γ✝ e'✝ e'✝ A✝
ih1 : CtxStrong env U (A✝ :: Γ✝) → IsDefEqStrong env U (A✝ :: Γ✝) e✝ e✝ B✝
ih2 : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ e'✝ e'✝ A✝
hΓ : CtxStrong env U Γ✝
he' : IsDefEqStrong env U Γ✝ e'✝ e'✝ A✝
w✝¹ : VLevel
hA : IsDefEqStrong env U Γ✝ A✝ A✝ (VExpr.sort w✝¹)
hΓ' : CtxStrong env U (A✝ :: Γ✝)
he : IsDefEqStrong env U (A✝ :: Γ✝) e✝ e✝ B✝
w✝ : VLevel
hB : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (VExpr.sort w✝)
⊢ IsDefEqStrong env U Γ✝ (app (lam A✝ e✝) e'✝) (inst e✝ e'✝) (inst B✝ e'✝)
Tactic:
exact .beta (hA.defeq.sort_r henv hΓ.defeq) (hB.defeq.sort_r henv hΓ'.defeq)
  hA hB he he' (he'.instN henv hΓ .zero hB hΓ) (he'.instN henv hΓ .zero he hΓ)
State after:
no goals

State before:
case eta
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
hctx : ∀ {Γ : List VExpr}, (OnCtx Γ fun Γ A => ∃ u, IsDefEqStrong env U Γ A A (VExpr.sort u)) → OnCtx Γ (IsType env U)
Γ✝ : List VExpr
e✝ A✝ B✝ : VExpr
a✝ : IsDefEq env U Γ✝ e✝ e✝ (VExpr.forallE A✝ B✝)
ih : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ e✝ e✝ (VExpr.forallE A✝ B✝)
hΓ : CtxStrong env U Γ✝
⊢ IsDefEqStrong env U Γ✝ (lam A✝ (app (lift e✝) (VExpr.bvar 0))) e✝ (VExpr.forallE A✝ B✝)
Tactic:
have he := ih hΓ
State after:
case eta
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
hctx : ∀ {Γ : List VExpr}, (OnCtx Γ fun Γ A => ∃ u, IsDefEqStrong env U Γ A A (VExpr.sort u)) → OnCtx Γ (IsType env U)
Γ✝ : List VExpr
e✝ A✝ B✝ : VExpr
a✝ : IsDefEq env U Γ✝ e✝ e✝ (VExpr.forallE A✝ B✝)
ih : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ e✝ e✝ (VExpr.forallE A✝ B✝)
hΓ : CtxStrong env U Γ✝
he : IsDefEqStrong env U Γ✝ e✝ e✝ (VExpr.forallE A✝ B✝)
⊢ IsDefEqStrong env U Γ✝ (lam A✝ (app (lift e✝) (VExpr.bvar 0))) e✝ (VExpr.forallE A✝ B✝)

State before:
case eta
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
hctx : ∀ {Γ : List VExpr}, (OnCtx Γ fun Γ A => ∃ u, IsDefEqStrong env U Γ A A (VExpr.sort u)) → OnCtx Γ (IsType env U)
Γ✝ : List VExpr
e✝ A✝ B✝ : VExpr
a✝ : IsDefEq env U Γ✝ e✝ e✝ (VExpr.forallE A✝ B✝)
ih : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ e✝ e✝ (VExpr.forallE A✝ B✝)
hΓ : CtxStrong env U Γ✝
he : IsDefEqStrong env U Γ✝ e✝ e✝ (VExpr.forallE A✝ B✝)
⊢ IsDefEqStrong env U Γ✝ (lam A✝ (app (lift e✝) (VExpr.bvar 0))) e✝ (VExpr.forallE A✝ B✝)
Tactic:
let ⟨_, hAB⟩ := he.isType' henv envIH hΓ
State after:
case eta
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
hctx : ∀ {Γ : List VExpr}, (OnCtx Γ fun Γ A => ∃ u, IsDefEqStrong env U Γ A A (VExpr.sort u)) → OnCtx Γ (IsType env U)
Γ✝ : List VExpr
e✝ A✝ B✝ : VExpr
a✝ : IsDefEq env U Γ✝ e✝ e✝ (VExpr.forallE A✝ B✝)
ih : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ e✝ e✝ (VExpr.forallE A✝ B✝)
hΓ : CtxStrong env U Γ✝
he : IsDefEqStrong env U Γ✝ e✝ e✝ (VExpr.forallE A✝ B✝)
w✝ : VLevel
hAB : IsDefEqStrong env U Γ✝ (VExpr.forallE A✝ B✝) (VExpr.forallE A✝ B✝) (VExpr.sort w✝)
⊢ IsDefEqStrong env U Γ✝ (lam A✝ (app (lift e✝) (VExpr.bvar 0))) e✝ (VExpr.forallE A✝ B✝)

State before:
case eta
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
hctx : ∀ {Γ : List VExpr}, (OnCtx Γ fun Γ A => ∃ u, IsDefEqStrong env U Γ A A (VExpr.sort u)) → OnCtx Γ (IsType env U)
Γ✝ : List VExpr
e✝ A✝ B✝ : VExpr
a✝ : IsDefEq env U Γ✝ e✝ e✝ (VExpr.forallE A✝ B✝)
ih : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ e✝ e✝ (VExpr.forallE A✝ B✝)
hΓ : CtxStrong env U Γ✝
he : IsDefEqStrong env U Γ✝ e✝ e✝ (VExpr.forallE A✝ B✝)
w✝ : VLevel
hAB : IsDefEqStrong env U Γ✝ (VExpr.forallE A✝ B✝) (VExpr.forallE A✝ B✝) (VExpr.sort w✝)
⊢ IsDefEqStrong env U Γ✝ (lam A✝ (app (lift e✝) (VExpr.bvar 0))) e✝ (VExpr.forallE A✝ B✝)
Tactic:
let ⟨⟨u, hA⟩, ⟨v, hB⟩⟩ := hAB.forallE_inv' henv envIH hΓ (.inl rfl)
State after:
case eta
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
hctx : ∀ {Γ : List VExpr}, (OnCtx Γ fun Γ A => ∃ u, IsDefEqStrong env U Γ A A (VExpr.sort u)) → OnCtx Γ (IsType env U)
Γ✝ : List VExpr
e✝ A✝ B✝ : VExpr
a✝ : IsDefEq env U Γ✝ e✝ e✝ (VExpr.forallE A✝ B✝)
ih : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ e✝ e✝ (VExpr.forallE A✝ B✝)
hΓ : CtxStrong env U Γ✝
he : IsDefEqStrong env U Γ✝ e✝ e✝ (VExpr.forallE A✝ B✝)
w✝ : VLevel
hAB : IsDefEqStrong env U Γ✝ (VExpr.forallE A✝ B✝) (VExpr.forallE A✝ B✝) (VExpr.sort w✝)
u : VLevel
hA : IsDefEqStrong env U Γ✝ A✝ A✝ (VExpr.sort u)
v : VLevel
hB : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (VExpr.sort v)
⊢ IsDefEqStrong env U Γ✝ (lam A✝ (app (lift e✝) (VExpr.bvar 0))) e✝ (VExpr.forallE A✝ B✝)

State before:
case eta
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
hctx : ∀ {Γ : List VExpr}, (OnCtx Γ fun Γ A => ∃ u, IsDefEqStrong env U Γ A A (VExpr.sort u)) → OnCtx Γ (IsType env U)
Γ✝ : List VExpr
e✝ A✝ B✝ : VExpr
a✝ : IsDefEq env U Γ✝ e✝ e✝ (VExpr.forallE A✝ B✝)
ih : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ e✝ e✝ (VExpr.forallE A✝ B✝)
hΓ : CtxStrong env U Γ✝
he : IsDefEqStrong env U Γ✝ e✝ e✝ (VExpr.forallE A✝ B✝)
w✝ : VLevel
hAB : IsDefEqStrong env U Γ✝ (VExpr.forallE A✝ B✝) (VExpr.forallE A✝ B✝) (VExpr.sort w✝)
u : VLevel
hA : IsDefEqStrong env U Γ✝ A✝ A✝ (VExpr.sort u)
v : VLevel
hB : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (VExpr.sort v)
⊢ IsDefEqStrong env U Γ✝ (lam A✝ (app (lift e✝) (VExpr.bvar 0))) e✝ (VExpr.forallE A✝ B✝)
Tactic:
have hΓ' : CtxStrong env U (_::_) := ⟨hΓ, _, hA⟩
State after:
case eta
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
hctx : ∀ {Γ : List VExpr}, (OnCtx Γ fun Γ A => ∃ u, IsDefEqStrong env U Γ A A (VExpr.sort u)) → OnCtx Γ (IsType env U)
Γ✝ : List VExpr
e✝ A✝ B✝ : VExpr
a✝ : IsDefEq env U Γ✝ e✝ e✝ (VExpr.forallE A✝ B✝)
ih : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ e✝ e✝ (VExpr.forallE A✝ B✝)
hΓ : CtxStrong env U Γ✝
he : IsDefEqStrong env U Γ✝ e✝ e✝ (VExpr.forallE A✝ B✝)
w✝ : VLevel
hAB : IsDefEqStrong env U Γ✝ (VExpr.forallE A✝ B✝) (VExpr.forallE A✝ B✝) (VExpr.sort w✝)
u : VLevel
hA : IsDefEqStrong env U Γ✝ A✝ A✝ (VExpr.sort u)
v : VLevel
hB : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (VExpr.sort v)
hΓ' : CtxStrong env U (A✝ :: Γ✝)
⊢ IsDefEqStrong env U Γ✝ (lam A✝ (app (lift e✝) (VExpr.bvar 0))) e✝ (VExpr.forallE A✝ B✝)

State before:
case eta
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
hctx : ∀ {Γ : List VExpr}, (OnCtx Γ fun Γ A => ∃ u, IsDefEqStrong env U Γ A A (VExpr.sort u)) → OnCtx Γ (IsType env U)
Γ✝ : List VExpr
e✝ A✝ B✝ : VExpr
a✝ : IsDefEq env U Γ✝ e✝ e✝ (VExpr.forallE A✝ B✝)
ih : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ e✝ e✝ (VExpr.forallE A✝ B✝)
hΓ : CtxStrong env U Γ✝
he : IsDefEqStrong env U Γ✝ e✝ e✝ (VExpr.forallE A✝ B✝)
w✝ : VLevel
hAB : IsDefEqStrong env U Γ✝ (VExpr.forallE A✝ B✝) (VExpr.forallE A✝ B✝) (VExpr.sort w✝)
u : VLevel
hA : IsDefEqStrong env U Γ✝ A✝ A✝ (VExpr.sort u)
v : VLevel
hB : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (VExpr.sort v)
hΓ' : CtxStrong env U (A✝ :: Γ✝)
⊢ IsDefEqStrong env U Γ✝ (lam A✝ (app (lift e✝) (VExpr.bvar 0))) e✝ (VExpr.forallE A✝ B✝)
Tactic:
exact .eta (hA.defeq.sort_r henv hΓ.defeq) (hB.defeq.sort_r henv hΓ'.defeq)
  hA hB (hB.weakN henv (.succ .one)) he (he.weakN henv .one)
State after:
no goals

State before:
case proofIrrel
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
hctx : ∀ {Γ : List VExpr}, (OnCtx Γ fun Γ A => ∃ u, IsDefEqStrong env U Γ A A (VExpr.sort u)) → OnCtx Γ (IsType env U)
Γ✝ : List VExpr
p✝ h✝ h'✝ : VExpr
a✝² : IsDefEq env U Γ✝ p✝ p✝ (VExpr.sort VLevel.zero)
a✝¹ : IsDefEq env U Γ✝ h✝ h✝ p✝
a✝ : IsDefEq env U Γ✝ h'✝ h'✝ p✝
ih1 : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ p✝ p✝ (VExpr.sort VLevel.zero)
ih2 : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ h✝ h✝ p✝
ih3 : CtxStrong env U Γ✝ → IsDefEqStrong env U Γ✝ h'✝ h'✝ p✝
hΓ : CtxStrong env U Γ✝
⊢ IsDefEqStrong env U Γ✝ h✝ h'✝ p✝
Tactic:
exact .proofIrrel (ih1 hΓ) (ih2 hΓ) (ih3 hΓ)
State after:
no goals

State before:
case extra
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
hctx : ∀ {Γ : List VExpr}, (OnCtx Γ fun Γ A => ∃ u, IsDefEqStrong env U Γ A A (VExpr.sort u)) → OnCtx Γ (IsType env U)
df✝ : VDefEq
ls✝ : List VLevel
Γ✝ : List VExpr
h1 : env.defeqs df✝
h2 : ∀ (l : VLevel), l ∈ ls✝ → VLevel.WF U l
h3 : List.length ls✝ = df✝.uvars
hΓ : CtxStrong env U Γ✝
⊢ IsDefEqStrong env U Γ✝ (VExpr.instL ls✝ df✝.lhs) (VExpr.instL ls✝ df✝.rhs) (VExpr.instL ls✝ df✝.type)
Tactic:
let ⟨⟨hl, ⟨_, ht⟩, _⟩, hr, _, _⟩ := envIH.2 h1
State after:
case extra
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
hctx : ∀ {Γ : List VExpr}, (OnCtx Γ fun Γ A => ∃ u, IsDefEqStrong env U Γ A A (VExpr.sort u)) → OnCtx Γ (IsType env U)
df✝ : VDefEq
ls✝ : List VLevel
Γ✝ : List VExpr
h1 : env.defeqs df✝
h2 : ∀ (l : VLevel), l ∈ ls✝ → VLevel.WF U l
h3 : List.length ls✝ = df✝.uvars
hΓ : CtxStrong env U Γ✝
hl : IsDefEqStrong env df✝.uvars [] df✝.lhs df✝.lhs df✝.type
w✝ : VLevel
ht : IsDefEqStrong env df✝.uvars [] df✝.type df✝.type (VExpr.sort w✝)
right✝¹ :
  ∀ (A B : VExpr),
    df✝.lhs = VExpr.forallE A B →
      (∃ u, IsDefEqStrong env df✝.uvars [] A A (VExpr.sort u)) ∧ ∃ u, IsDefEqStrong env df✝.uvars [A] B B (VExpr.sort u)
hr : IsDefEqStrong env df✝.uvars [] df✝.rhs df✝.rhs df✝.type
left✝ : ∃ u, IsDefEqStrong env df✝.uvars [] df✝.type df✝.type (VExpr.sort u)
right✝ :
  ∀ (A B : VExpr),
    df✝.rhs = VExpr.forallE A B →
      (∃ u, IsDefEqStrong env df✝.uvars [] A A (VExpr.sort u)) ∧ ∃ u, IsDefEqStrong env df✝.uvars [A] B B (VExpr.sort u)
⊢ IsDefEqStrong env U Γ✝ (VExpr.instL ls✝ df✝.lhs) (VExpr.instL ls✝ df✝.rhs) (VExpr.instL ls✝ df✝.type)

State before:
case extra
env : VEnv
henv : Ordered env
envIH : OnTypes env (EnvStrong env)
U : Nat
Γ : List VExpr
e1 e2 A : VExpr
hctx : ∀ {Γ : List VExpr}, (OnCtx Γ fun Γ A => ∃ u, IsDefEqStrong env U Γ A A (VExpr.sort u)) → OnCtx Γ (IsType env U)
df✝ : VDefEq
ls✝ : List VLevel
Γ✝ : List VExpr
h1 : env.defeqs df✝
h2 : ∀ (l : VLevel), l ∈ ls✝ → VLevel.WF U l
h3 : List.length ls✝ = df✝.uvars
hΓ : CtxStrong env U Γ✝
hl : IsDefEqStrong env df✝.uvars [] df✝.lhs df✝.lhs df✝.type
w✝ : VLevel
ht : IsDefEqStrong env df✝.uvars [] df✝.type df✝.type (VExpr.sort w✝)
right✝¹ :
  ∀ (A B : VExpr),
    df✝.lhs = VExpr.forallE A B →
      (∃ u, IsDefEqStrong env df✝.uvars [] A A (VExpr.sort u)) ∧ ∃ u, IsDefEqStrong env df✝.uvars [A] B B (VExpr.sort u)
hr : IsDefEqStrong env df✝.uvars [] df✝.rhs df✝.rhs df✝.type
left✝ : ∃ u, IsDefEqStrong env df✝.uvars [] df✝.type df✝.type (VExpr.sort u)
right✝ :
  ∀ (A B : VExpr),
    df✝.rhs = VExpr.forallE A B →
      (∃ u, IsDefEqStrong env df✝.uvars [] A A (VExpr.sort u)) ∧ ∃ u, IsDefEqStrong env df✝.uvars [A] B B (VExpr.sort u)
⊢ IsDefEqStrong env U Γ✝ (VExpr.instL ls✝ df✝.lhs) (VExpr.instL ls✝ df✝.rhs) (VExpr.instL ls✝ df✝.type)
Tactic:
exact .extra h1 h2 h3 (.inst h2) (ht.instL h2)
  (hl.instL h2) (hr.instL h2) ((hl.instL h2).weak0 henv) ((hr.instL h2).weak0 henv)
State after:
no goals