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