const Inj0 : set set const Inj1 : set set axiom Inj0_Inj1_neq: !x:set.!y:set.Inj0 x != Inj1 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 axiom FalseE: ~ False const setsum : set set set const ordsucc : set set const Empty : set axiom Inj1_pair_1_eq: Inj1 = setsum (ordsucc Empty) axiom Inj0_pair_0_eq: Inj0 = setsum Empty axiom Inj1_inj: !x:set.!y:set.Inj1 x = Inj1 y -> x = y 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 (ordsucc Empty) z iIn setsum x y -> z iIn y