Theorem: Lean4Lean.VExpr.lift'_depth_zero (Lean4Lean/Theory/VExpr.lean)

State before:
l : Lift
e : VExpr
H : Lift.depth l = 0
⊢ lift' e l = e
Tactic:
induction e generalizing l <;> simp_all [liftVar_depth_zero]
State after:
no goals