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

State before:
e : VExpr
n1 n2 k : Nat
⊢ unliftN e (n1 + n2) k = unliftN (unliftN e n1 k) n2 k
Tactic:
induction n1 generalizing e <;> simp [unliftN, Nat.succ_add, *]
State after:
no goals