const In : set set prop term iIn = In infix iIn 2000 2000 term Subq = \x:set.\y:set.!z:set.z iIn x -> z iIn y const Repl : set (set set) set const Inj1 : set set term Inj0 = \x:set.Repl x Inj1 const Unj : set set axiom Unj_Inj1_eq: !x:set.Unj (Inj1 x) = x axiom ReplE_impred: !x:set.!f:set set.!y:set.y iIn Repl x f -> !P:prop.(!z:set.z iIn x -> y = f z -> P) -> P const setminus : set set set const nIn : set set prop axiom setminusE: !x:set.!y:set.!z:set.z iIn setminus x y -> z iIn x & nIn z y axiom ReplI: !x:set.!f:set set.!y:set.y iIn x -> f y iIn Repl x f const Sing : set set const Empty : set axiom Inj1NE2: !x:set.nIn (Inj1 x) (Sing Empty) axiom setminusI: !x:set.!y:set.!z:set.z iIn x -> nIn z y -> z iIn setminus x y axiom set_ext: !x:set.!y:set.Subq x y -> Subq y x -> x = y axiom Unj_eq: !x:set.Unj x = Repl (setminus x (Sing Empty)) Unj lemma !x:set.!y:set.!z:set.!w:set.y = Unj z -> w iIn x -> z = Inj1 w -> y = w -> y iIn x claim !x:set.Unj (Inj0 x) = x