Theorem: Lean4Lean.VEnv.IsDefEq.inductionU1
Proof state before:
case appDF
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✝ : 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✝)
a✝² : IsDefEqStrong env U Γ✝ f✝ f'✝ (VExpr.forallE A✝ B✝)
a✝¹ : IsDefEqStrong env U Γ✝ a✝⁷ a'✝ A✝
a✝ : IsDefEqStrong env U Γ✝ (inst B✝ a✝⁷) (inst B✝ a'✝) (VExpr.sort v✝)
a_ih✝¹ :
  HasTypeU1 env U defEq Γ✝ A✝ (VExpr.sort u✝) ∧
    HasTypeU1 env U defEq Γ✝ A✝ (VExpr.sort u✝) ∧ IsDefEqU1 env U hasType Γ✝ A✝ A✝
a_ih✝ :
  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✝
ihf :
  HasTypeU1 env U defEq Γ✝ f✝ (VExpr.forallE A✝ B✝) ∧
    HasTypeU1 env U defEq Γ✝ f'✝ (VExpr.forallE A✝ B✝) ∧ IsDefEqU1 env U hasType Γ✝ f✝ f'✝
iha : HasTypeU1 env U defEq Γ✝ a✝⁷ A✝ ∧ HasTypeU1 env U defEq Γ✝ a'✝ A✝ ∧ IsDefEqU1 env U hasType Γ✝ a✝⁷ a'✝
ihBa :
  HasTypeU1 env U defEq Γ✝ (inst B✝ a✝⁷) (VExpr.sort v✝) ∧
    HasTypeU1 env U defEq Γ✝ (inst B✝ a'✝) (VExpr.sort v✝) ∧ IsDefEqU1 env U hasType Γ✝ (inst B✝ a✝⁷) (inst B✝ a'✝)
⊢ HasTypeU1 env U defEq Γ✝ (app f✝ a✝⁷) (inst B✝ a✝⁷) ∧
    HasTypeU1 env U defEq Γ✝ (app f'✝ a'✝) (inst B✝ a✝⁷) ∧ IsDefEqU1 env U hasType Γ✝ (app f✝ a✝⁷) (app f'✝ a'✝)
Tactic:
let ⟨hf, hf', ff⟩ := ihf
Proof state after:
case appDF
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✝ : 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✝)
a✝² : IsDefEqStrong env U Γ✝ f✝ f'✝ (VExpr.forallE A✝ B✝)
a✝¹ : IsDefEqStrong env U Γ✝ a✝⁷ a'✝ A✝
a✝ : IsDefEqStrong env U Γ✝ (inst B✝ a✝⁷) (inst B✝ a'✝) (VExpr.sort v✝)
a_ih✝¹ :
  HasTypeU1 env U defEq Γ✝ A✝ (VExpr.sort u✝) ∧
    HasTypeU1 env U defEq Γ✝ A✝ (VExpr.sort u✝) ∧ IsDefEqU1 env U hasType Γ✝ A✝ A✝
a_ih✝ :
  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✝
ihf :
  HasTypeU1 env U defEq Γ✝ f✝ (VExpr.forallE A✝ B✝) ∧
    HasTypeU1 env U defEq Γ✝ f'✝ (VExpr.forallE A✝ B✝) ∧ IsDefEqU1 env U hasType Γ✝ f✝ f'✝
iha : HasTypeU1 env U defEq Γ✝ a✝⁷ A✝ ∧ HasTypeU1 env U defEq Γ✝ a'✝ A✝ ∧ IsDefEqU1 env U hasType Γ✝ a✝⁷ a'✝
ihBa :
  HasTypeU1 env U defEq Γ✝ (inst B✝ a✝⁷) (VExpr.sort v✝) ∧
    HasTypeU1 env U defEq Γ✝ (inst B✝ a'✝) (VExpr.sort v✝) ∧ IsDefEqU1 env U hasType Γ✝ (inst B✝ a✝⁷) (inst B✝ a'✝)
hf : HasTypeU1 env U defEq Γ✝ f✝ (VExpr.forallE A✝ B✝)
hf' : HasTypeU1 env U defEq Γ✝ f'✝ (VExpr.forallE A✝ B✝)
ff : IsDefEqU1 env U hasType Γ✝ f✝ f'✝
⊢ HasTypeU1 env U defEq Γ✝ (app f✝ a✝⁷) (inst B✝ a✝⁷) ∧
    HasTypeU1 env U defEq Γ✝ (app f'✝ a'✝) (inst B✝ a✝⁷) ∧ IsDefEqU1 env U hasType Γ✝ (app f✝ a✝⁷) (app f'✝ a'✝)