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 In_rec_i_eq: !P:set (set set) set.(!x:set.!f:set set.!f2:set set.(!y:set.y iIn x -> f y = f2 y) -> P x f = P x f2) -> !x:set.In_rec_i P x = P x (In_rec_i P) claim (!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)))