Theorem: Lean4Lean.VExpr.liftN'_liftN_lo (Lean4Lean/Theory/VExpr.lean)

State before:
e : VExpr
n k : Nat
⊢ liftN n (liftN k e) k = liftN (n + k) e
Tactic:
simpa [Nat.add_comm] using liftN'_liftN' (n1 := k) (n2 := n) (Nat.zero_le _) (Nat.le_refl _)
State after:
no goals