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

State before:
n : Nat
⊢ pred (succ n) = n
Tactic:
simp [pred]
State after:
no goals