Theorem: Lean4Lean.VEnv.IsDefEq.inductionU1
Proof state before:
case lamDF
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
e1 e2 A : VExpr
defEq hasType : List VExpr → VExpr → VExpr → Prop
hty : ∀ {Γ : List VExpr} {e A : VExpr}, HasTypeU1 env U defEq Γ e A → hasType Γ e A
hdf :
  ∀ {Γ : List VExpr} {e1 e2 A1 A2 : VExpr},
    HasTypeU1 env U defEq Γ e1 A1 → HasTypeU1 env U defEq Γ e2 A2 → IsDefEqU1 env U hasType Γ e1 e2 → defEq Γ e1 e2
Γ✝ : List VExpr
A✝ A'✝ : VExpr
u✝ : VLevel
B✝ : VExpr
v✝ : VLevel
body✝ body'✝ : 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✝² : IsDefEqStrong env U (A'✝ :: Γ✝) B✝ B✝ (VExpr.sort v✝)
a✝¹ : IsDefEqStrong env U (A✝ :: Γ✝) body✝ body'✝ B✝
a✝ : IsDefEqStrong env U (A'✝ :: Γ✝) body✝ body'✝ B✝
ihA :
  HasTypeU1 env U defEq Γ✝ A✝ (VExpr.sort u✝) ∧
    HasTypeU1 env U defEq Γ✝ A'✝ (VExpr.sort u✝) ∧ IsDefEqU1 env U hasType Γ✝ A✝ A'✝
ihB :
  HasTypeU1 env U defEq (A✝ :: Γ✝) B✝ (VExpr.sort v✝) ∧
    HasTypeU1 env U defEq (A✝ :: Γ✝) B✝ (VExpr.sort v✝) ∧ IsDefEqU1 env U hasType (A✝ :: Γ✝) B✝ B✝
ihB' :
  HasTypeU1 env U defEq (A'✝ :: Γ✝) B✝ (VExpr.sort v✝) ∧
    HasTypeU1 env U defEq (A'✝ :: Γ✝) B✝ (VExpr.sort v✝) ∧ IsDefEqU1 env U hasType (A'✝ :: Γ✝) B✝ B✝
ihb :
  HasTypeU1 env U defEq (A✝ :: Γ✝) body✝ B✝ ∧
    HasTypeU1 env U defEq (A✝ :: Γ✝) body'✝ B✝ ∧ IsDefEqU1 env U hasType (A✝ :: Γ✝) body✝ body'✝
ihb' :
  HasTypeU1 env U defEq (A'✝ :: Γ✝) body✝ B✝ ∧
    HasTypeU1 env U defEq (A'✝ :: Γ✝) body'✝ B✝ ∧ IsDefEqU1 env U hasType (A'✝ :: Γ✝) body✝ body'✝
⊢ HasTypeU1 env U defEq Γ✝ (lam A✝ body✝) (VExpr.forallE A✝ B✝) ∧
    HasTypeU1 env U defEq Γ✝ (lam A'✝ body'✝) (VExpr.forallE A✝ B✝) ∧
      IsDefEqU1 env U hasType Γ✝ (lam A✝ body✝) (lam A'✝ body'✝)
Tactic:
refine ⟨.lam ihA.1 ihb.1, .defeq ?_ <| .lam ihA.2.1 ihb'.2.1, .lamDF ihA.2.2 ihb.2.2⟩
Proof state after:
case lamDF
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
e1 e2 A : VExpr
defEq hasType : List VExpr → VExpr → VExpr → Prop
hty : ∀ {Γ : List VExpr} {e A : VExpr}, HasTypeU1 env U defEq Γ e A → hasType Γ e A
hdf :
  ∀ {Γ : List VExpr} {e1 e2 A1 A2 : VExpr},
    HasTypeU1 env U defEq Γ e1 A1 → HasTypeU1 env U defEq Γ e2 A2 → IsDefEqU1 env U hasType Γ e1 e2 → defEq Γ e1 e2
Γ✝ : List VExpr
A✝ A'✝ : VExpr
u✝ : VLevel
B✝ : VExpr
v✝ : VLevel
body✝ body'✝ : 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✝² : IsDefEqStrong env U (A'✝ :: Γ✝) B✝ B✝ (VExpr.sort v✝)
a✝¹ : IsDefEqStrong env U (A✝ :: Γ✝) body✝ body'✝ B✝
a✝ : IsDefEqStrong env U (A'✝ :: Γ✝) body✝ body'✝ B✝
ihA :
  HasTypeU1 env U defEq Γ✝ A✝ (VExpr.sort u✝) ∧
    HasTypeU1 env U defEq Γ✝ A'✝ (VExpr.sort u✝) ∧ IsDefEqU1 env U hasType Γ✝ A✝ A'✝
ihB :
  HasTypeU1 env U defEq (A✝ :: Γ✝) B✝ (VExpr.sort v✝) ∧
    HasTypeU1 env U defEq (A✝ :: Γ✝) B✝ (VExpr.sort v✝) ∧ IsDefEqU1 env U hasType (A✝ :: Γ✝) B✝ B✝
ihB' :
  HasTypeU1 env U defEq (A'✝ :: Γ✝) B✝ (VExpr.sort v✝) ∧
    HasTypeU1 env U defEq (A'✝ :: Γ✝) B✝ (VExpr.sort v✝) ∧ IsDefEqU1 env U hasType (A'✝ :: Γ✝) B✝ B✝
ihb :
  HasTypeU1 env U defEq (A✝ :: Γ✝) body✝ B✝ ∧
    HasTypeU1 env U defEq (A✝ :: Γ✝) body'✝ B✝ ∧ IsDefEqU1 env U hasType (A✝ :: Γ✝) body✝ body'✝
ihb' :
  HasTypeU1 env U defEq (A'✝ :: Γ✝) body✝ B✝ ∧
    HasTypeU1 env U defEq (A'✝ :: Γ✝) body'✝ B✝ ∧ IsDefEqU1 env U hasType (A'✝ :: Γ✝) body✝ body'✝
⊢ defEq Γ✝ (VExpr.forallE A'✝ B✝) (VExpr.forallE A✝ B✝)