Theorem: Lean4Lean.VEnv.IsDefEqStrong.weakN
Proof state before:
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))
Tactic:
have ih5 : IsDefEqStrong _ _ _ _ _ (liftN n (lift (forallE ..)) _) := ih5 W.succ
Proof state after:
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 Γ Γ'
ih5 :
  IsDefEqStrong env U (liftN n a k :: Γ') (liftN n (lift e) (k + 1)) (liftN n (lift e) (k + 1))
    (liftN n (lift (forallE a B)) (k + 1))
⊢ 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))