const In : set set prop term iIn = In infix iIn 2000 2000 const Inj1 : set set const setsum : set set set axiom Inj1_setsum: !x:set.!y:set.!z:set.z iIn y -> Inj1 z iIn setsum x y const ordsucc : set set const Empty : set axiom Inj1_pair_1_eq: Inj1 = setsum (ordsucc Empty) claim !x:set.!y:set.!z:set.z iIn y -> setsum (ordsucc Empty) z iIn setsum x y