const In_rec_i : (set (set set) set) set set const binunion : set set set const Sing : set set const Empty : set const Repl : set (set set) set term Inj1 = In_rec_i \x:set.\f:set set.binunion (Sing Empty) (Repl x f) 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) -> binunion (Sing Empty) (Repl x f) = binunion (Sing Empty) (Repl x f2)) -> !x:set.In_rec_i (\y:set.\f:set set.binunion (Sing Empty) (Repl y f)) x = binunion (Sing Empty) (Repl x (In_rec_i \y:set.\f:set set.binunion (Sing Empty) (Repl y f)))