Theorem: Lean4Lean.VEnv.IsDefEq.induction1
Proof state before:
case appDF
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
e1 e2 A : VExpr
defEq : List VExpr → VExpr → VExpr → VExpr → Prop
hasType : List VExpr → VExpr → VExpr → Prop
hty : ∀ {Γ : List VExpr} {e A : VExpr}, HasType1 env U defEq Γ e A → hasType Γ e A
hdf : ∀ {Γ : List VExpr} {e1 e2 A : VExpr}, IsDefEq1 env U hasType defEq Γ e1 e2 A → defEq Γ e1 e2 A
Γ✝ : 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✝¹ :
  HasType1 env U defEq Γ✝ A✝ (VExpr.sort u✝) ∧
    HasType1 env U defEq Γ✝ A✝ (VExpr.sort u✝) ∧ IsDefEq1 env U hasType defEq Γ✝ A✝ A✝ (VExpr.sort u✝)
a_ih✝ :
  HasType1 env U defEq (A✝ :: Γ✝) B✝ (VExpr.sort v✝) ∧
    HasType1 env U defEq (A✝ :: Γ✝) B✝ (VExpr.sort v✝) ∧ IsDefEq1 env U hasType defEq (A✝ :: Γ✝) B✝ B✝ (VExpr.sort v✝)
ihf :
  HasType1 env U defEq Γ✝ f✝ (VExpr.forallE A✝ B✝) ∧
    HasType1 env U defEq Γ✝ f'✝ (VExpr.forallE A✝ B✝) ∧ IsDefEq1 env U hasType defEq Γ✝ f✝ f'✝ (VExpr.forallE A✝ B✝)
iha : HasType1 env U defEq Γ✝ a✝⁷ A✝ ∧ HasType1 env U defEq Γ✝ a'✝ A✝ ∧ IsDefEq1 env U hasType defEq Γ✝ a✝⁷ a'✝ A✝
ihBa :
  HasType1 env U defEq Γ✝ (inst B✝ a✝⁷) (VExpr.sort v✝) ∧
    HasType1 env U defEq Γ✝ (inst B✝ a'✝) (VExpr.sort v✝) ∧
      IsDefEq1 env U hasType defEq Γ✝ (inst B✝ a✝⁷) (inst B✝ a'✝) (VExpr.sort v✝)
⊢ HasType1 env U defEq Γ✝ (app f✝ a✝⁷) (inst B✝ a✝⁷) ∧
    HasType1 env U defEq Γ✝ (app f'✝ a'✝) (inst B✝ a✝⁷) ∧
      IsDefEq1 env U hasType defEq Γ✝ (app f✝ a✝⁷) (app f'✝ a'✝) (inst B✝ 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 : List VExpr → VExpr → VExpr → VExpr → Prop
hasType : List VExpr → VExpr → VExpr → Prop
hty : ∀ {Γ : List VExpr} {e A : VExpr}, HasType1 env U defEq Γ e A → hasType Γ e A
hdf : ∀ {Γ : List VExpr} {e1 e2 A : VExpr}, IsDefEq1 env U hasType defEq Γ e1 e2 A → defEq Γ e1 e2 A
Γ✝ : 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✝¹ :
  HasType1 env U defEq Γ✝ A✝ (VExpr.sort u✝) ∧
    HasType1 env U defEq Γ✝ A✝ (VExpr.sort u✝) ∧ IsDefEq1 env U hasType defEq Γ✝ A✝ A✝ (VExpr.sort u✝)
a_ih✝ :
  HasType1 env U defEq (A✝ :: Γ✝) B✝ (VExpr.sort v✝) ∧
    HasType1 env U defEq (A✝ :: Γ✝) B✝ (VExpr.sort v✝) ∧ IsDefEq1 env U hasType defEq (A✝ :: Γ✝) B✝ B✝ (VExpr.sort v✝)
ihf :
  HasType1 env U defEq Γ✝ f✝ (VExpr.forallE A✝ B✝) ∧
    HasType1 env U defEq Γ✝ f'✝ (VExpr.forallE A✝ B✝) ∧ IsDefEq1 env U hasType defEq Γ✝ f✝ f'✝ (VExpr.forallE A✝ B✝)
iha : HasType1 env U defEq Γ✝ a✝⁷ A✝ ∧ HasType1 env U defEq Γ✝ a'✝ A✝ ∧ IsDefEq1 env U hasType defEq Γ✝ a✝⁷ a'✝ A✝
ihBa :
  HasType1 env U defEq Γ✝ (inst B✝ a✝⁷) (VExpr.sort v✝) ∧
    HasType1 env U defEq Γ✝ (inst B✝ a'✝) (VExpr.sort v✝) ∧
      IsDefEq1 env U hasType defEq Γ✝ (inst B✝ a✝⁷) (inst B✝ a'✝) (VExpr.sort v✝)
hf : HasType1 env U defEq Γ✝ f✝ (VExpr.forallE A✝ B✝)
hf' : HasType1 env U defEq Γ✝ f'✝ (VExpr.forallE A✝ B✝)
ff : IsDefEq1 env U hasType defEq Γ✝ f✝ f'✝ (VExpr.forallE A✝ B✝)
⊢ HasType1 env U defEq Γ✝ (app f✝ a✝⁷) (inst B✝ a✝⁷) ∧
    HasType1 env U defEq Γ✝ (app f'✝ a'✝) (inst B✝ a✝⁷) ∧
      IsDefEq1 env U hasType defEq Γ✝ (app f✝ a✝⁷) (app f'✝ a'✝) (inst B✝ a✝⁷)