const If_i : prop set set set const In : set set prop term iIn = In infix iIn 2000 2000 const Repl : set (set set) set const Eps_i : (set prop) set const Empty : set term Sep = \x:set.\p:set prop.If_i (?y:set.y iIn x & p y) (Repl x \y:set.If_i (p y) y (Eps_i \z:set.z iIn x & p z)) Empty axiom ReplI: !x:set.!f:set set.!y:set.y iIn x -> f y iIn Repl x f var x:set var p:set prop var y:set hyp y iIn x hyp p y claim If_i (p y) y (Eps_i \z:set.z iIn x & p z) = y -> y iIn Repl x \z:set.If_i (p z) z (Eps_i \w:set.w iIn x & p w)