Relevant arithmetic axioms and theorems I could prove so far include
Z$(x)=0$
S$(x)\not=0,$S$(x)$=S$(y)\rightarrow x=y$
wffs state that = is an equivalence relation
$x=y\rightarrow \mbox f(...x...)=\mbox f(...y...)$ where f is any expression that represents a primitive recursive function
the first-order induction scheme
$x=0\lor\exists y.x=\mbox S(y)$
~~$x=0\rightarrow x=0$
I know induction should be used but I am not yet able to get to (~~x=Sy)→x=Sy from (~~x=y)→x=y. Thanks.