Theorem: Lean4Lean.VEnv.IsDefEq.app_inv'
Proof state before:
case appDF
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
e1 e2 V f a : VExpr
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
B✝ : VExpr
v✝ : VLevel
f✝ f'✝ a✝⁵ a'✝ : VExpr
a✝⁴ : VLevel.WF U u✝
a✝³ : VLevel.WF U v✝
a✝² : IsDefEqStrong env U Γ✝ A✝ A✝ (VExpr.sort u✝)
a✝¹ : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (VExpr.sort v✝)
h1 : IsDefEqStrong env U Γ✝ f✝ f'✝ (VExpr.forallE A✝ B✝)
h2 : IsDefEqStrong env U Γ✝ a✝⁵ a'✝ A✝
a✝ : IsDefEqStrong env U Γ✝ (inst B✝ a✝⁵) (inst B✝ a'✝) (VExpr.sort v✝)
a_ih✝⁴ : A✝ = app f a ∨ A✝ = app f a → ∃ A B, HasType env U Γ✝ f (VExpr.forallE A B) ∧ HasType env U Γ✝ a A
a_ih✝³ :
  B✝ = app f a ∨ B✝ = app f a → ∃ A B, HasType env U (A✝ :: Γ✝) f (VExpr.forallE A B) ∧ HasType env U (A✝ :: Γ✝) a A
a_ih✝² : f✝ = app f a ∨ f'✝ = app f a → ∃ A B, HasType env U Γ✝ f (VExpr.forallE A B) ∧ HasType env U Γ✝ a A
a_ih✝¹ : a✝⁵ = app f a ∨ a'✝ = app f a → ∃ A B, HasType env U Γ✝ f (VExpr.forallE A B) ∧ HasType env U Γ✝ a A
a_ih✝ :
  inst B✝ a✝⁵ = app f a ∨ inst B✝ a'✝ = app f a → ∃ A B, HasType env U Γ✝ f (VExpr.forallE A B) ∧ HasType env U Γ✝ a A
eq : app f✝ a✝⁵ = app f a ∨ app f'✝ a'✝ = app f a
⊢ ∃ A B, HasType env U Γ✝ f (VExpr.forallE A B) ∧ HasType env U Γ✝ a A
Tactic:
obtain ⟨⟨⟩⟩ | ⟨⟨⟩⟩ := eq
Proof state after:
case appDF.inl.refl
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
e1 e2 V f a : VExpr
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
B✝ : VExpr
v✝ : VLevel
f'✝ a'✝ : VExpr
a✝⁴ : VLevel.WF U u✝
a✝³ : VLevel.WF U v✝
a✝² : IsDefEqStrong env U Γ✝ A✝ A✝ (VExpr.sort u✝)
a✝¹ : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (VExpr.sort v✝)
a_ih✝⁴ : A✝ = app f a ∨ A✝ = app f a → ∃ A B, HasType env U Γ✝ f (VExpr.forallE A B) ∧ HasType env U Γ✝ a A
a_ih✝³ :
  B✝ = app f a ∨ B✝ = app f a → ∃ A B, HasType env U (A✝ :: Γ✝) f (VExpr.forallE A B) ∧ HasType env U (A✝ :: Γ✝) a A
h1 : IsDefEqStrong env U Γ✝ f f'✝ (VExpr.forallE A✝ B✝)
a_ih✝² : f = app f a ∨ f'✝ = app f a → ∃ A B, HasType env U Γ✝ f (VExpr.forallE A B) ∧ HasType env U Γ✝ a A
h2 : IsDefEqStrong env U Γ✝ a a'✝ A✝
a✝ : IsDefEqStrong env U Γ✝ (inst B✝ a) (inst B✝ a'✝) (VExpr.sort v✝)
a_ih✝¹ : a = app f a ∨ a'✝ = app f a → ∃ A B, HasType env U Γ✝ f (VExpr.forallE A B) ∧ HasType env U Γ✝ a A
a_ih✝ :
  inst B✝ a = app f a ∨ inst B✝ a'✝ = app f a → ∃ A B, HasType env U Γ✝ f (VExpr.forallE A B) ∧ HasType env U Γ✝ a A
⊢ ∃ A B, HasType env U Γ✝ f (VExpr.forallE A B) ∧ HasType env U Γ✝ a A

case appDF.inr.refl
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
e1 e2 V f a : VExpr
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
B✝ : VExpr
v✝ : VLevel
f✝ a✝⁵ : VExpr
a✝⁴ : VLevel.WF U u✝
a✝³ : VLevel.WF U v✝
a✝² : IsDefEqStrong env U Γ✝ A✝ A✝ (VExpr.sort u✝)
a✝¹ : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (VExpr.sort v✝)
a_ih✝⁴ : A✝ = app f a ∨ A✝ = app f a → ∃ A B, HasType env U Γ✝ f (VExpr.forallE A B) ∧ HasType env U Γ✝ a A
a_ih✝³ :
  B✝ = app f a ∨ B✝ = app f a → ∃ A B, HasType env U (A✝ :: Γ✝) f (VExpr.forallE A B) ∧ HasType env U (A✝ :: Γ✝) a A
h1 : IsDefEqStrong env U Γ✝ f✝ f (VExpr.forallE A✝ B✝)
a_ih✝² : f✝ = app f a ∨ f = app f a → ∃ A B, HasType env U Γ✝ f (VExpr.forallE A B) ∧ HasType env U Γ✝ a A
h2 : IsDefEqStrong env U Γ✝ a✝⁵ a A✝
a✝ : IsDefEqStrong env U Γ✝ (inst B✝ a✝⁵) (inst B✝ a) (VExpr.sort v✝)
a_ih✝¹ : a✝⁵ = app f a ∨ a = app f a → ∃ A B, HasType env U Γ✝ f (VExpr.forallE A B) ∧ HasType env U Γ✝ a A
a_ih✝ :
  inst B✝ a✝⁵ = app f a ∨ inst B✝ a = app f a → ∃ A B, HasType env U Γ✝ f (VExpr.forallE A B) ∧ HasType env U Γ✝ a A
⊢ ∃ A B, HasType env U Γ✝ f (VExpr.forallE A B) ∧ HasType env U Γ✝ a A