Theorem: Lean4Lean.VEnv.IsDefEq.lam_inv'
Proof state before:
case lamDF
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
e1 e2 V A body : VExpr
Γ✝ : List VExpr
A✝ A'✝ : VExpr
u✝ : VLevel
B✝ : VExpr
v✝ : VLevel
body✝ body'✝ : VExpr
a✝³ : VLevel.WF U u✝
a✝² : VLevel.WF U v✝
h1 : IsDefEqStrong env U Γ✝ A✝ A'✝ (VExpr.sort u✝)
a✝¹ : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (VExpr.sort v✝)
a✝ : IsDefEqStrong env U (A'✝ :: Γ✝) B✝ B✝ (VExpr.sort v✝)
h4 : IsDefEqStrong env U (A✝ :: Γ✝) body✝ body'✝ B✝
h5 : IsDefEqStrong env U (A'✝ :: Γ✝) body✝ body'✝ B✝
a_ih✝⁴ : A✝ = lam A body ∨ A'✝ = lam A body → IsType env U Γ✝ A ∧ WF env U (A :: Γ✝) body
a_ih✝³ : B✝ = lam A body ∨ B✝ = lam A body → IsType env U (A✝ :: Γ✝) A ∧ WF env U (A :: A✝ :: Γ✝) body
a_ih✝² : B✝ = lam A body ∨ B✝ = lam A body → IsType env U (A'✝ :: Γ✝) A ∧ WF env U (A :: A'✝ :: Γ✝) body
a_ih✝¹ : body✝ = lam A body ∨ body'✝ = lam A body → IsType env U (A✝ :: Γ✝) A ∧ WF env U (A :: A✝ :: Γ✝) body
a_ih✝ : body✝ = lam A body ∨ body'✝ = lam A body → IsType env U (A'✝ :: Γ✝) A ∧ WF env U (A :: A'✝ :: Γ✝) body
eq : lam A✝ body✝ = lam A body ∨ lam A'✝ body'✝ = lam A body
⊢ IsType env U Γ✝ A ∧ WF env U (A :: Γ✝) body
Tactic:
obtain ⟨⟨⟩⟩ | ⟨⟨⟩⟩ := eq
Proof state after:
case lamDF.inl.refl
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
e1 e2 V A body : VExpr
Γ✝ : List VExpr
A'✝ : VExpr
u✝ : VLevel
B✝ : VExpr
v✝ : VLevel
body'✝ : VExpr
a✝³ : VLevel.WF U u✝
a✝² : VLevel.WF U v✝
a✝¹ : IsDefEqStrong env U (A'✝ :: Γ✝) B✝ B✝ (VExpr.sort v✝)
a_ih✝⁴ : B✝ = lam A body ∨ B✝ = lam A body → IsType env U (A'✝ :: Γ✝) A ∧ WF env U (A :: A'✝ :: Γ✝) body
h1 : IsDefEqStrong env U Γ✝ A A'✝ (VExpr.sort u✝)
a✝ : IsDefEqStrong env U (A :: Γ✝) B✝ B✝ (VExpr.sort v✝)
a_ih✝³ : A = lam A body ∨ A'✝ = lam A body → IsType env U Γ✝ A ∧ WF env U (A :: Γ✝) body
a_ih✝² : B✝ = lam A body ∨ B✝ = lam A body → IsType env U (A :: Γ✝) A ∧ WF env U (A :: A :: Γ✝) body
h5 : IsDefEqStrong env U (A'✝ :: Γ✝) body body'✝ B✝
a_ih✝¹ : body = lam A body ∨ body'✝ = lam A body → IsType env U (A'✝ :: Γ✝) A ∧ WF env U (A :: A'✝ :: Γ✝) body
h4 : IsDefEqStrong env U (A :: Γ✝) body body'✝ B✝
a_ih✝ : body = lam A body ∨ body'✝ = lam A body → IsType env U (A :: Γ✝) A ∧ WF env U (A :: A :: Γ✝) body
⊢ IsType env U Γ✝ A ∧ WF env U (A :: Γ✝) body

case lamDF.inr.refl
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
e1 e2 V A body : VExpr
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
B✝ : VExpr
v✝ : VLevel
body✝ : VExpr
a✝³ : VLevel.WF U u✝
a✝² : VLevel.WF U v✝
a✝¹ : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (VExpr.sort v✝)
a_ih✝⁴ : B✝ = lam A body ∨ B✝ = lam A body → IsType env U (A✝ :: Γ✝) A ∧ WF env U (A :: A✝ :: Γ✝) body
h1 : IsDefEqStrong env U Γ✝ A✝ A (VExpr.sort u✝)
a✝ : IsDefEqStrong env U (A :: Γ✝) B✝ B✝ (VExpr.sort v✝)
a_ih✝³ : A✝ = lam A body ∨ A = lam A body → IsType env U Γ✝ A ∧ WF env U (A :: Γ✝) body
a_ih✝² : B✝ = lam A body ∨ B✝ = lam A body → IsType env U (A :: Γ✝) A ∧ WF env U (A :: A :: Γ✝) body
h4 : IsDefEqStrong env U (A✝ :: Γ✝) body✝ body B✝
a_ih✝¹ : body✝ = lam A body ∨ body = lam A body → IsType env U (A✝ :: Γ✝) A ∧ WF env U (A :: A✝ :: Γ✝) body
h5 : IsDefEqStrong env U (A :: Γ✝) body✝ body B✝
a_ih✝ : body✝ = lam A body ∨ body = lam A body → IsType env U (A :: Γ✝) A ∧ WF env U (A :: A :: Γ✝) body
⊢ IsType env U Γ✝ A ∧ WF env U (A :: Γ✝) body