Theorem: Lean4Lean.Lift.consN_consN (Lean4Lean/Theory/VExpr.lean)

State before:
l : Lift
a b : Nat
⊢ consN (consN l a) b = consN l (a + b)
Tactic:
induction b <;> simp [*]
State after:
no goals