const In_rec_i : (set (set set) set) set set const Repl : set (set set) set const setminus : set set set const Sing : set set const Empty : set term Unj = In_rec_i \x:set.Repl (setminus x (Sing Empty)) const In : set set prop term iIn = In infix iIn 2000 2000 axiom setminusE1: !x:set.!y:set.!z:set.z iIn setminus x y -> z iIn x axiom ReplEq_ext: !x:set.!f:set set.!f2:set set.(!y:set.y iIn x -> f y = f2 y) -> Repl x f = Repl x f2 lemma (!x:set.!f:set set.!f2:set set.(!y:set.y iIn x -> f y = f2 y) -> Repl (setminus x (Sing Empty)) f = Repl (setminus x (Sing Empty)) f2) -> !x:set.In_rec_i (\y:set.Repl (setminus y (Sing Empty))) x = Repl (setminus x (Sing Empty)) (In_rec_i \y:set.Repl (setminus y (Sing Empty))) claim !x:set.Unj x = Repl (setminus x (Sing Empty)) \y:set.Unj y