Theorem: Lean4Lean.VLevel.succ_congr (Lean4Lean/Theory/VLevel.lean)

State before:
a b : VLevel
h : a ≈ b
⊢ succ a ≈ succ b
Tactic:
simpa [equiv_def, eval] using h
State after:
no goals