Theorem: Lean4Lean.VEnv.IsDefEq.app_inv'
Proof state before:
case beta
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
e✝ e'✝ : VExpr
a✝⁴ : VLevel.WF U u✝
a✝³ : VLevel.WF U v✝
hA : IsDefEqStrong env U Γ✝ A✝ A✝ (VExpr.sort u✝)
a✝² : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (VExpr.sort v✝)
he : IsDefEqStrong env U (A✝ :: Γ✝) e✝ e✝ B✝
he' : IsDefEqStrong env U Γ✝ e'✝ e'✝ A✝
a✝¹ : IsDefEqStrong env U Γ✝ (inst B✝ e'✝) (inst B✝ e'✝) (VExpr.sort v✝)
a✝ : IsDefEqStrong env U Γ✝ (inst e✝ e'✝) (inst e✝ e'✝) (inst B✝ e'✝)
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✝² :
  e✝ = app f a ∨ e✝ = app f a → ∃ A B, HasType env U (A✝ :: Γ✝) f (VExpr.forallE A B) ∧ HasType env U (A✝ :: Γ✝) a A
a_ih✝¹ : e'✝ = app f a ∨ e'✝ = app f a → ∃ A B, HasType env U Γ✝ f (VExpr.forallE A B) ∧ HasType env U Γ✝ a A
a_ih✝ :
  inst B✝ e'✝ = app f a ∨ inst B✝ e'✝ = app f a → ∃ A B, HasType env U Γ✝ f (VExpr.forallE A B) ∧ HasType env U Γ✝ a A
ihee :
  inst e✝ e'✝ = app f a ∨ inst e✝ e'✝ = app f a → ∃ A B, HasType env U Γ✝ f (VExpr.forallE A B) ∧ HasType env U Γ✝ a A
eq : app (lam A✝ e✝) e'✝ = app f a ∨ inst e✝ e'✝ = app f a
⊢ ∃ A B, HasType env U Γ✝ f (VExpr.forallE A B) ∧ HasType env U Γ✝ a A
Tactic:
obtain ⟨⟨⟩⟩ | eq := eq
Proof state after:
case beta.inl.refl
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
e1 e2 V a : VExpr
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
B✝ : VExpr
v✝ : VLevel
e✝ : VExpr
a✝⁴ : VLevel.WF U u✝
a✝³ : VLevel.WF U v✝
hA : IsDefEqStrong env U Γ✝ A✝ A✝ (VExpr.sort u✝)
a✝² : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (VExpr.sort v✝)
he : IsDefEqStrong env U (A✝ :: Γ✝) e✝ e✝ B✝
a_ih✝⁴ :
  A✝ = app (lam A✝ e✝) a ∨ A✝ = app (lam A✝ e✝) a →
    ∃ A B, HasType env U Γ✝ (lam A✝ e✝) (VExpr.forallE A B) ∧ HasType env U Γ✝ a A
a_ih✝³ :
  B✝ = app (lam A✝ e✝) a ∨ B✝ = app (lam A✝ e✝) a →
    ∃ A B, HasType env U (A✝ :: Γ✝) (lam A✝ e✝) (VExpr.forallE A B) ∧ HasType env U (A✝ :: Γ✝) a A
a_ih✝² :
  e✝ = app (lam A✝ e✝) a ∨ e✝ = app (lam A✝ e✝) a →
    ∃ A B, HasType env U (A✝ :: Γ✝) (lam A✝ e✝) (VExpr.forallE A B) ∧ HasType env U (A✝ :: Γ✝) a A
he' : IsDefEqStrong env U Γ✝ a a A✝
a✝¹ : IsDefEqStrong env U Γ✝ (inst B✝ a) (inst B✝ a) (VExpr.sort v✝)
a✝ : IsDefEqStrong env U Γ✝ (inst e✝ a) (inst e✝ a) (inst B✝ a)
a_ih✝¹ :
  a = app (lam A✝ e✝) a ∨ a = app (lam A✝ e✝) a →
    ∃ A B, HasType env U Γ✝ (lam A✝ e✝) (VExpr.forallE A B) ∧ HasType env U Γ✝ a A
a_ih✝ :
  inst B✝ a = app (lam A✝ e✝) a ∨ inst B✝ a = app (lam A✝ e✝) a →
    ∃ A B, HasType env U Γ✝ (lam A✝ e✝) (VExpr.forallE A B) ∧ HasType env U Γ✝ a A
ihee :
  inst e✝ a = app (lam A✝ e✝) a ∨ inst e✝ a = app (lam A✝ e✝) a →
    ∃ A B, HasType env U Γ✝ (lam A✝ e✝) (VExpr.forallE A B) ∧ HasType env U Γ✝ a A
⊢ ∃ A B, HasType env U Γ✝ (lam A✝ e✝) (VExpr.forallE A B) ∧ HasType env U Γ✝ a A

case beta.inr
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
e✝ e'✝ : VExpr
a✝⁴ : VLevel.WF U u✝
a✝³ : VLevel.WF U v✝
hA : IsDefEqStrong env U Γ✝ A✝ A✝ (VExpr.sort u✝)
a✝² : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (VExpr.sort v✝)
he : IsDefEqStrong env U (A✝ :: Γ✝) e✝ e✝ B✝
he' : IsDefEqStrong env U Γ✝ e'✝ e'✝ A✝
a✝¹ : IsDefEqStrong env U Γ✝ (inst B✝ e'✝) (inst B✝ e'✝) (VExpr.sort v✝)
a✝ : IsDefEqStrong env U Γ✝ (inst e✝ e'✝) (inst e✝ e'✝) (inst B✝ e'✝)
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✝² :
  e✝ = app f a ∨ e✝ = app f a → ∃ A B, HasType env U (A✝ :: Γ✝) f (VExpr.forallE A B) ∧ HasType env U (A✝ :: Γ✝) a A
a_ih✝¹ : e'✝ = app f a ∨ e'✝ = app f a → ∃ A B, HasType env U Γ✝ f (VExpr.forallE A B) ∧ HasType env U Γ✝ a A
a_ih✝ :
  inst B✝ e'✝ = app f a ∨ inst B✝ e'✝ = app f a → ∃ A B, HasType env U Γ✝ f (VExpr.forallE A B) ∧ HasType env U Γ✝ a A
ihee :
  inst e✝ e'✝ = app f a ∨ inst e✝ e'✝ = app f a → ∃ A B, HasType env U Γ✝ f (VExpr.forallE A B) ∧ HasType env U Γ✝ a A
eq : inst e✝ e'✝ = app f a
⊢ ∃ A B, HasType env U Γ✝ f (VExpr.forallE A B) ∧ HasType env U Γ✝ a A