proposition: Theorem succ_eq_succ_of_eq (a b : mynat) : a = b → succ(a) = succ(b).
proof: Proof. intro f. rewrite f. reflexivity. Qed.
imports: Unicode.Utf8 Game.Mynat.Definition Game.Mynat.Add Game.World.Addition Game.World.Proposition Game.World.AdvancedProposition Setoid