const In : set set prop term iIn = In infix iIn 2000 2000 const ordsucc : set set const Empty : set axiom cases_2: !x:set.x iIn ordsucc (ordsucc Empty) -> !p:set prop.p Empty -> p (ordsucc Empty) -> p x axiom ordsuccE: !x:set.!y:set.y iIn ordsucc x -> y iIn x | y = x claim !x:set.x iIn ordsucc (ordsucc (ordsucc Empty)) -> !p:set prop.p Empty -> p (ordsucc Empty) -> p (ordsucc (ordsucc Empty)) -> p x