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

State before:
n i k : Nat
⊢ liftVar n (i + 1) (k + 1) = liftVar n i k + 1
Tactic:
simp [liftVar, Nat.succ_lt_succ_iff]
State after:
n i k : Nat
⊢ (if i < k then i + 1 else n + (i + 1)) = (if i < k then i else n + i) + 1

State before:
n i k : Nat
⊢ (if i < k then i + 1 else n + (i + 1)) = (if i < k then i else n + i) + 1
Tactic:
split <;> simp [Nat.add_assoc]
State after:
no goals