const In : set set prop term iIn = In infix iIn 2000 2000 const setsum : set set set const Inj0 : set set const Inj1 : set set axiom setsum_Inj_inv: !x:set.!y:set.!z:set.z iIn setsum x y -> (?w:set.w iIn x & z = Inj0 w) | ?w:set.w iIn y & z = Inj1 w const ordsucc : set set const Empty : set axiom Inj1_pair_1_eq: Inj1 = setsum (ordsucc Empty) axiom Inj0_pair_0_eq: Inj0 = setsum Empty claim !x:set.!y:set.!z:set.z iIn setsum x y -> (?w:set.w iIn x & z = setsum Empty w) | ?w:set.w iIn y & z = setsum (ordsucc Empty) w