const ordsucc : set set axiom ordsucc_inj: !x:set.!y:set.ordsucc x = ordsucc y -> x = y claim !x:set.!y:set.x != y -> ordsucc x != ordsucc y