Theorem: Lean4Lean.VExpr.levelWF_liftN (Lean4Lean/Theory/VExpr.lean)

State before:
n : Nat
e : VExpr
k U : Nat
⊢ LevelWF U (liftN n e k) ↔ LevelWF U e
Tactic:
induction e generalizing k <;> simp [liftN, LevelWF, *]
State after:
no goals