const In : set set prop term iIn = In infix iIn 2000 2000 term Subq = \x:set.\y:set.!z:set.z iIn x -> z iIn y const Repl : set (set set) set axiom ReplE_impred: !x:set.!f:set set.!y:set.y iIn Repl x f -> !P:prop.(!z:set.z iIn x -> y = f z -> P) -> P axiom ReplI: !x:set.!f:set set.!y:set.y iIn x -> f y iIn Repl x f axiom set_ext: !x:set.!y:set.Subq x y -> Subq y x -> x = y claim !p:set prop.!f:set set.!f2:set set.(!x:set.p x -> f2 (f x) = x) -> !x:set.(!y:set.y iIn x -> p y) -> Repl (Repl x f) f2 = x