const In : set set prop term iIn = In infix iIn 2000 2000 axiom In_no2cycle: !x:set.!y:set.x iIn y -> ~ y iIn x axiom FalseE: ~ False const ordsucc : set set axiom ordsuccE: !x:set.!y:set.y iIn ordsucc x -> y iIn x | y = x var x:set var y:set hyp ordsucc x = ordsucc y hyp x iIn y claim y iIn ordsucc x -> x = y