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

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