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

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