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