theorem nateq (_p1 _p2: wff): $ (_p1 <-> _p2) -> nat _p1 = nat _p2 $;
(_p1 <-> _p2) -> (_p1 <-> _p2)
(_p1 <-> _p2) -> nat _p1 = nat _p2