Theorem: Lean4Lean.VEnv.IsDefEq.lam_inv'
Proof state before:
case eta
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
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✝)
a✝¹ : IsDefEqStrong env U (lift A✝ :: A✝ :: Γ✝) (liftN 1 B✝ 1) (liftN 1 B✝ 1) (VExpr.sort v✝)
a✝ : IsDefEqStrong env U Γ✝ e✝ e✝ (VExpr.forallE A✝ B✝)
he' : IsDefEqStrong env U (A✝ :: Γ✝) (lift e✝) (lift e✝) (VExpr.forallE (lift A✝) (liftN 1 B✝ 1))
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✝¹ :
  liftN 1 B✝ 1 = lam A body ∨ liftN 1 B✝ 1 = lam A body →
    IsType env U (lift A✝ :: A✝ :: Γ✝) A ∧ WF env U (A :: lift A✝ :: A✝ :: Γ✝) body
ih : e✝ = lam A body ∨ e✝ = lam A body → IsType env U Γ✝ A ∧ WF env U (A :: Γ✝) body
a_ih✝ : lift e✝ = lam A body ∨ lift e✝ = lam A body → IsType env U (A✝ :: Γ✝) A ∧ WF env U (A :: A✝ :: Γ✝) body
eq : lam A✝ (app (lift e✝) (VExpr.bvar 0)) = lam A body ∨ e✝ = lam A body
⊢ IsType env U Γ✝ A ∧ WF env U (A :: Γ✝) body
Tactic:
obtain ⟨⟨⟩⟩ | eq := eq
Proof state after:
case eta.inl.refl
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
e1 e2 V A : VExpr
Γ✝ : List 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✝)
a✝¹ : IsDefEqStrong env U (lift A :: A :: Γ✝) (liftN 1 B✝ 1) (liftN 1 B✝ 1) (VExpr.sort v✝)
a✝ : IsDefEqStrong env U Γ✝ e✝ e✝ (VExpr.forallE A B✝)
he' : IsDefEqStrong env U (A :: Γ✝) (lift e✝) (lift e✝) (VExpr.forallE (lift A) (liftN 1 B✝ 1))
ih :
  e✝ = lam A (app (lift e✝) (VExpr.bvar 0)) ∨ e✝ = lam A (app (lift e✝) (VExpr.bvar 0)) →
    IsType env U Γ✝ A ∧ WF env U (A :: Γ✝) (app (lift e✝) (VExpr.bvar 0))
a_ih✝³ :
  A = lam A (app (lift e✝) (VExpr.bvar 0)) ∨ A = lam A (app (lift e✝) (VExpr.bvar 0)) →
    IsType env U Γ✝ A ∧ WF env U (A :: Γ✝) (app (lift e✝) (VExpr.bvar 0))
a_ih✝² :
  B✝ = lam A (app (lift e✝) (VExpr.bvar 0)) ∨ B✝ = lam A (app (lift e✝) (VExpr.bvar 0)) →
    IsType env U (A :: Γ✝) A ∧ WF env U (A :: A :: Γ✝) (app (lift e✝) (VExpr.bvar 0))
a_ih✝¹ :
  liftN 1 B✝ 1 = lam A (app (lift e✝) (VExpr.bvar 0)) ∨ liftN 1 B✝ 1 = lam A (app (lift e✝) (VExpr.bvar 0)) →
    IsType env U (lift A :: A :: Γ✝) A ∧ WF env U (A :: lift A :: A :: Γ✝) (app (lift e✝) (VExpr.bvar 0))
a_ih✝ :
  lift e✝ = lam A (app (lift e✝) (VExpr.bvar 0)) ∨ lift e✝ = lam A (app (lift e✝) (VExpr.bvar 0)) →
    IsType env U (A :: Γ✝) A ∧ WF env U (A :: A :: Γ✝) (app (lift e✝) (VExpr.bvar 0))
⊢ IsType env U Γ✝ A ∧ WF env U (A :: Γ✝) (app (lift e✝) (VExpr.bvar 0))

case eta.inr
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
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✝)
a✝¹ : IsDefEqStrong env U (lift A✝ :: A✝ :: Γ✝) (liftN 1 B✝ 1) (liftN 1 B✝ 1) (VExpr.sort v✝)
a✝ : IsDefEqStrong env U Γ✝ e✝ e✝ (VExpr.forallE A✝ B✝)
he' : IsDefEqStrong env U (A✝ :: Γ✝) (lift e✝) (lift e✝) (VExpr.forallE (lift A✝) (liftN 1 B✝ 1))
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✝¹ :
  liftN 1 B✝ 1 = lam A body ∨ liftN 1 B✝ 1 = lam A body →
    IsType env U (lift A✝ :: A✝ :: Γ✝) A ∧ WF env U (A :: lift A✝ :: A✝ :: Γ✝) body
ih : e✝ = lam A body ∨ e✝ = lam A body → IsType env U Γ✝ A ∧ WF env U (A :: Γ✝) body
a_ih✝ : lift e✝ = lam A body ∨ lift e✝ = lam A body → IsType env U (A✝ :: Γ✝) A ∧ WF env U (A :: A✝ :: Γ✝) body
eq : e✝ = lam A body
⊢ IsType env U Γ✝ A ∧ WF env U (A :: Γ✝) body