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

State before:
l : Lift
n : Nat
H : Lift.depth l = 0
⊢ Lift.liftVar l n = n
Tactic:
induction l generalizing n <;> [skip; skip; cases n] <;> simp_all [Lift.depth]
State after:
no goals