Theorem: Lean4Lean.VExpr.lift'_consN_skipN (Lean4Lean/Theory/VExpr.lean)

State before:
n : Nat
e : VExpr
k : Nat
⊢ liftN n e k = lift' e (Lift.consN (Lift.skipN n) k)
Tactic:
induction e generalizing k <;> simp [liftN, liftVar_consN_skipN, *]
State after:
no goals