Theorem: Lean4Lean.VEnv.IsDefEq.induction1
Proof state before:
case eta
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
e✝ : 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 (lift A✝ :: A✝ :: Γ✝) (liftN 1 B✝ 1) (liftN 1 B✝ 1) (VExpr.sort v✝)
a✝¹ : IsDefEqStrong env U Γ✝ e✝ e✝ (VExpr.forallE A✝ B✝)
a✝ : IsDefEqStrong env U (A✝ :: Γ✝) (lift e✝) (lift e✝) (VExpr.forallE (lift A✝) (liftN 1 B✝ 1))
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✝)
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✝)
a_ih✝ :
  HasType1 env U defEq (lift A✝ :: A✝ :: Γ✝) (liftN 1 B✝ 1) (VExpr.sort v✝) ∧
    HasType1 env U defEq (lift A✝ :: A✝ :: Γ✝) (liftN 1 B✝ 1) (VExpr.sort v✝) ∧
      IsDefEq1 env U hasType defEq (lift A✝ :: A✝ :: Γ✝) (liftN 1 B✝ 1) (liftN 1 B✝ 1) (VExpr.sort v✝)
ihe :
  HasType1 env U defEq Γ✝ e✝ (VExpr.forallE A✝ B✝) ∧
    HasType1 env U defEq Γ✝ e✝ (VExpr.forallE A✝ B✝) ∧ IsDefEq1 env U hasType defEq Γ✝ e✝ e✝ (VExpr.forallE A✝ B✝)
ihe' :
  HasType1 env U defEq (A✝ :: Γ✝) (lift e✝) (VExpr.forallE (lift A✝) (liftN 1 B✝ 1)) ∧
    HasType1 env U defEq (A✝ :: Γ✝) (lift e✝) (VExpr.forallE (lift A✝) (liftN 1 B✝ 1)) ∧
      IsDefEq1 env U hasType defEq (A✝ :: Γ✝) (lift e✝) (lift e✝) (VExpr.forallE (lift A✝) (liftN 1 B✝ 1))
⊢ HasType1 env U defEq Γ✝ (lam A✝ (app (lift e✝) (VExpr.bvar 0))) (VExpr.forallE A✝ B✝) ∧
    HasType1 env U defEq Γ✝ e✝ (VExpr.forallE A✝ B✝) ∧
      IsDefEq1 env U hasType defEq Γ✝ (lam A✝ (app (lift e✝) (VExpr.bvar 0))) e✝ (VExpr.forallE A✝ B✝)
Tactic:
have := HasType1.app ihe'.1 (.bvar .zero)
Proof state after:
case eta
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
e✝ : 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 (lift A✝ :: A✝ :: Γ✝) (liftN 1 B✝ 1) (liftN 1 B✝ 1) (VExpr.sort v✝)
a✝¹ : IsDefEqStrong env U Γ✝ e✝ e✝ (VExpr.forallE A✝ B✝)
a✝ : IsDefEqStrong env U (A✝ :: Γ✝) (lift e✝) (lift e✝) (VExpr.forallE (lift A✝) (liftN 1 B✝ 1))
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✝)
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✝)
a_ih✝ :
  HasType1 env U defEq (lift A✝ :: A✝ :: Γ✝) (liftN 1 B✝ 1) (VExpr.sort v✝) ∧
    HasType1 env U defEq (lift A✝ :: A✝ :: Γ✝) (liftN 1 B✝ 1) (VExpr.sort v✝) ∧
      IsDefEq1 env U hasType defEq (lift A✝ :: A✝ :: Γ✝) (liftN 1 B✝ 1) (liftN 1 B✝ 1) (VExpr.sort v✝)
ihe :
  HasType1 env U defEq Γ✝ e✝ (VExpr.forallE A✝ B✝) ∧
    HasType1 env U defEq Γ✝ e✝ (VExpr.forallE A✝ B✝) ∧ IsDefEq1 env U hasType defEq Γ✝ e✝ e✝ (VExpr.forallE A✝ B✝)
ihe' :
  HasType1 env U defEq (A✝ :: Γ✝) (lift e✝) (VExpr.forallE (lift A✝) (liftN 1 B✝ 1)) ∧
    HasType1 env U defEq (A✝ :: Γ✝) (lift e✝) (VExpr.forallE (lift A✝) (liftN 1 B✝ 1)) ∧
      IsDefEq1 env U hasType defEq (A✝ :: Γ✝) (lift e✝) (lift e✝) (VExpr.forallE (lift A✝) (liftN 1 B✝ 1))
this : HasType1 env U defEq (A✝ :: Γ✝) (app (lift e✝) (VExpr.bvar 0)) (inst (liftN 1 B✝ 1) (VExpr.bvar 0))
⊢ HasType1 env U defEq Γ✝ (lam A✝ (app (lift e✝) (VExpr.bvar 0))) (VExpr.forallE A✝ B✝) ∧
    HasType1 env U defEq Γ✝ e✝ (VExpr.forallE A✝ B✝) ∧
      IsDefEq1 env U hasType defEq Γ✝ (lam A✝ (app (lift e✝) (VExpr.bvar 0))) e✝ (VExpr.forallE A✝ B✝)