const Inj0 : set set axiom Inj0_inj: !x:set.!y:set.Inj0 x = Inj0 y -> x = y axiom exandE_i: !p:set prop.!q:set prop.(?x:set.p x & q x) -> !P:prop.(!x:set.p x -> q x -> P) -> P const setsum : set set set const Empty : set axiom Inj0_pair_0_eq: Inj0 = setsum Empty const Inj1 : set set axiom Inj0_Inj1_neq: !x:set.!y:set.Inj0 x != Inj1 y axiom FalseE: ~ False const ordsucc : set set axiom Inj1_pair_1_eq: Inj1 = setsum (ordsucc Empty) const In : set set prop term iIn = In infix iIn 2000 2000 axiom pairE: !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 claim !x:set.!y:set.!z:set.setsum Empty z iIn setsum x y -> z iIn x