const In : set set prop term iIn = In infix iIn 2000 2000 const Subq : set set prop const Repl : set (set set) set axiom ReplEq_ext_sub: !x:set.!f:set set.!f2:set set.(!y:set.y iIn x -> f y = f2 y) -> Subq (Repl x f) (Repl x f2) axiom set_ext: !x:set.!y:set.Subq x y -> Subq y x -> x = y claim !x:set.!f:set set.!f2:set set.(!y:set.y iIn x -> f y = f2 y) -> Repl x f = Repl x f2