Theorem: Lean4Lean.VEnv.IsDefEqStrong.weakN
Proof state before:
case eta
env : VEnv
henv : Ordered env
n : Nat
Γ✝ : List VExpr
U : Nat
e1 e2 A : VExpr
Γ : List VExpr
a : VExpr
u : VLevel
B : VExpr
v : VLevel
e : VExpr
h1 : VLevel.WF U u
h2 : VLevel.WF U v
a✝⁴ : IsDefEqStrong env U Γ a a (sort u)
a✝³ : IsDefEqStrong env U (a :: Γ) B B (sort v)
a✝² : IsDefEqStrong env U (lift a :: a :: Γ) (liftN 1 B 1) (liftN 1 B 1) (sort v)
a✝¹ : IsDefEqStrong env U Γ e e (forallE a B)
a✝ : IsDefEqStrong env U (a :: Γ) (lift e) (lift e) (forallE (lift a) (liftN 1 B 1))
ih1 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k Γ Γ' → IsDefEqStrong env U Γ' (liftN n a k) (liftN n a k) (liftN n (sort u) k)
ih2 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k (a :: Γ) Γ' → IsDefEqStrong env U Γ' (liftN n B k) (liftN n B k) (liftN n (sort v) k)
ih3 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k (lift a :: a :: Γ) Γ' →
      IsDefEqStrong env U Γ' (liftN n (liftN 1 B 1) k) (liftN n (liftN 1 B 1) k) (liftN n (sort v) k)
ih4 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k Γ Γ' → IsDefEqStrong env U Γ' (liftN n e k) (liftN n e k) (liftN n (forallE a B) k)
ih5 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k (a :: Γ) Γ' →
      IsDefEqStrong env U Γ' (liftN n (lift e) k) (liftN n (lift e) k) (liftN n (forallE (lift a) (liftN 1 B 1)) k)
k : Nat
Γ' : List VExpr
W : Ctx.LiftN n k Γ Γ'
⊢ IsDefEqStrong env U Γ' (liftN n (lam a (app (lift e) (VExpr.bvar 0))) k) (liftN n e k) (liftN n (forallE a B) k)
Tactic:
have := IsDefEqStrong.eta h1 h2 (ih1 W) (ih2 W.succ) ?_ (ih4 W) ?_
Proof state after:
case eta.refine_3
env : VEnv
henv : Ordered env
n : Nat
Γ✝ : List VExpr
U : Nat
e1 e2 A : VExpr
Γ : List VExpr
a : VExpr
u : VLevel
B : VExpr
v : VLevel
e : VExpr
h1 : VLevel.WF U u
h2 : VLevel.WF U v
a✝⁴ : IsDefEqStrong env U Γ a a (sort u)
a✝³ : IsDefEqStrong env U (a :: Γ) B B (sort v)
a✝² : IsDefEqStrong env U (lift a :: a :: Γ) (liftN 1 B 1) (liftN 1 B 1) (sort v)
a✝¹ : IsDefEqStrong env U Γ e e (forallE a B)
a✝ : IsDefEqStrong env U (a :: Γ) (lift e) (lift e) (forallE (lift a) (liftN 1 B 1))
ih1 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k Γ Γ' → IsDefEqStrong env U Γ' (liftN n a k) (liftN n a k) (liftN n (sort u) k)
ih2 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k (a :: Γ) Γ' → IsDefEqStrong env U Γ' (liftN n B k) (liftN n B k) (liftN n (sort v) k)
ih3 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k (lift a :: a :: Γ) Γ' →
      IsDefEqStrong env U Γ' (liftN n (liftN 1 B 1) k) (liftN n (liftN 1 B 1) k) (liftN n (sort v) k)
ih4 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k Γ Γ' → IsDefEqStrong env U Γ' (liftN n e k) (liftN n e k) (liftN n (forallE a B) k)
ih5 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k (a :: Γ) Γ' →
      IsDefEqStrong env U Γ' (liftN n (lift e) k) (liftN n (lift e) k) (liftN n (forallE (lift a) (liftN 1 B 1)) k)
k : Nat
Γ' : List VExpr
W : Ctx.LiftN n k Γ Γ'
this :
  IsDefEqStrong env U Γ' (lam (liftN n a k) (app (lift (liftN n e k)) (VExpr.bvar 0))) (liftN n e k)
    (forallE (liftN n a k) (liftN n B (k + 1)))
⊢ IsDefEqStrong env U Γ' (liftN n (lam a (app (lift e) (VExpr.bvar 0))) k) (liftN n e k) (liftN n (forallE a B) k)

case eta.refine_1
env : VEnv
henv : Ordered env
n : Nat
Γ✝ : List VExpr
U : Nat
e1 e2 A : VExpr
Γ : List VExpr
a : VExpr
u : VLevel
B : VExpr
v : VLevel
e : VExpr
h1 : VLevel.WF U u
h2 : VLevel.WF U v
a✝⁴ : IsDefEqStrong env U Γ a a (sort u)
a✝³ : IsDefEqStrong env U (a :: Γ) B B (sort v)
a✝² : IsDefEqStrong env U (lift a :: a :: Γ) (liftN 1 B 1) (liftN 1 B 1) (sort v)
a✝¹ : IsDefEqStrong env U Γ e e (forallE a B)
a✝ : IsDefEqStrong env U (a :: Γ) (lift e) (lift e) (forallE (lift a) (liftN 1 B 1))
ih1 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k Γ Γ' → IsDefEqStrong env U Γ' (liftN n a k) (liftN n a k) (liftN n (sort u) k)
ih2 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k (a :: Γ) Γ' → IsDefEqStrong env U Γ' (liftN n B k) (liftN n B k) (liftN n (sort v) k)
ih3 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k (lift a :: a :: Γ) Γ' →
      IsDefEqStrong env U Γ' (liftN n (liftN 1 B 1) k) (liftN n (liftN 1 B 1) k) (liftN n (sort v) k)
ih4 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k Γ Γ' → IsDefEqStrong env U Γ' (liftN n e k) (liftN n e k) (liftN n (forallE a B) k)
ih5 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k (a :: Γ) Γ' →
      IsDefEqStrong env U Γ' (liftN n (lift e) k) (liftN n (lift e) k) (liftN n (forallE (lift a) (liftN 1 B 1)) k)
k : Nat
Γ' : List VExpr
W : Ctx.LiftN n k Γ Γ'
⊢ IsDefEqStrong env U (lift (liftN n a k) :: liftN n a k :: Γ') (liftN 1 (liftN n B (k + 1)) 1)
    (liftN 1 (liftN n B (k + 1)) 1) (sort v)

case eta.refine_2
env : VEnv
henv : Ordered env
n : Nat
Γ✝ : List VExpr
U : Nat
e1 e2 A : VExpr
Γ : List VExpr
a : VExpr
u : VLevel
B : VExpr
v : VLevel
e : VExpr
h1 : VLevel.WF U u
h2 : VLevel.WF U v
a✝⁴ : IsDefEqStrong env U Γ a a (sort u)
a✝³ : IsDefEqStrong env U (a :: Γ) B B (sort v)
a✝² : IsDefEqStrong env U (lift a :: a :: Γ) (liftN 1 B 1) (liftN 1 B 1) (sort v)
a✝¹ : IsDefEqStrong env U Γ e e (forallE a B)
a✝ : IsDefEqStrong env U (a :: Γ) (lift e) (lift e) (forallE (lift a) (liftN 1 B 1))
ih1 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k Γ Γ' → IsDefEqStrong env U Γ' (liftN n a k) (liftN n a k) (liftN n (sort u) k)
ih2 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k (a :: Γ) Γ' → IsDefEqStrong env U Γ' (liftN n B k) (liftN n B k) (liftN n (sort v) k)
ih3 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k (lift a :: a :: Γ) Γ' →
      IsDefEqStrong env U Γ' (liftN n (liftN 1 B 1) k) (liftN n (liftN 1 B 1) k) (liftN n (sort v) k)
ih4 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k Γ Γ' → IsDefEqStrong env U Γ' (liftN n e k) (liftN n e k) (liftN n (forallE a B) k)
ih5 :
  ∀ {k : Nat} {Γ' : List VExpr},
    Ctx.LiftN n k (a :: Γ) Γ' →
      IsDefEqStrong env U Γ' (liftN n (lift e) k) (liftN n (lift e) k) (liftN n (forallE (lift a) (liftN 1 B 1)) k)
k : Nat
Γ' : List VExpr
W : Ctx.LiftN n k Γ Γ'
⊢ IsDefEqStrong env U (liftN n a k :: Γ') (lift (liftN n e k)) (lift (liftN n e k))
    (forallE (lift (liftN n a k)) (liftN 1 (liftN n B (k + 1)) 1))