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

State before:
e : VExpr
k : Nat
⊢ liftN 0 e k = e
Tactic:
induction e generalizing k <;> simp [liftN, liftVar, *]
State after:
no goals