Theorem: MyNat.succ_eq_succ_of_eq (TheoremProvingLean/inductive_types.lean)

State before:
a b : Nat
⊢ a = b → succ a = succ b
Tactic:
intro h
State after:
a b : Nat
h : a = b
⊢ succ a = succ b

State before:
a b : Nat
h : a = b
⊢ succ a = succ b
Tactic:
rw [h]
State after:
no goals