Theorem: Lean4Lean.VEnv.IsDefEq.induction1
Proof state before:
case lamDF
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✝ 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 :
  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✝)
ihB :
  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✝)
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✝)
ihb :
  HasType1 env U defEq (A✝ :: Γ✝) body✝ B✝ ∧
    HasType1 env U defEq (A✝ :: Γ✝) body'✝ B✝ ∧ IsDefEq1 env U hasType defEq (A✝ :: Γ✝) body✝ body'✝ B✝
ihb' :
  HasType1 env U defEq (A'✝ :: Γ✝) body✝ B✝ ∧
    HasType1 env U defEq (A'✝ :: Γ✝) body'✝ B✝ ∧ IsDefEq1 env U hasType defEq (A'✝ :: Γ✝) body✝ body'✝ B✝
⊢ HasType1 env U defEq Γ✝ (lam A✝ body✝) (VExpr.forallE A✝ B✝) ∧
    HasType1 env U defEq Γ✝ (lam A'✝ body'✝) (VExpr.forallE A✝ B✝) ∧
      IsDefEq1 env U hasType defEq Γ✝ (lam A✝ body✝) (lam A'✝ body'✝) (VExpr.forallE A✝ B✝)
Tactic:
refine ⟨.lam ihA.1 ihb.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 : 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✝ 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 :
  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✝)
ihB :
  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✝)
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✝)
ihb :
  HasType1 env U defEq (A✝ :: Γ✝) body✝ B✝ ∧
    HasType1 env U defEq (A✝ :: Γ✝) body'✝ B✝ ∧ IsDefEq1 env U hasType defEq (A✝ :: Γ✝) body✝ body'✝ B✝
ihb' :
  HasType1 env U defEq (A'✝ :: Γ✝) body✝ B✝ ∧
    HasType1 env U defEq (A'✝ :: Γ✝) body'✝ B✝ ∧ IsDefEq1 env U hasType defEq (A'✝ :: Γ✝) body✝ body'✝ B✝
⊢ HasType1 env U defEq Γ✝ (lam A'✝ body'✝) (VExpr.forallE A✝ B✝)