Theorem: MyNat.succ_inj' (TheoremProvingLean/inductive_types.lean)

State before:
a b : Nat
hs : succ a = succ b
⊢ a = b
Tactic:
exact succ_inj hs
State after:
no goals