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

State before:
⊢ 1 = succ zero
Tactic:
rfl
State after:
no goals