const ReplSep : set (set prop) (set set) set const setsum : set set set const proj1 : set set term ap = \x:set.\y:set.ReplSep x (\z:set.?w:set.z = setsum y w) proj1 axiom proj1_pair_eq: !x:set.!y:set.proj1 (setsum x y) = y const In : set set prop term iIn = In infix iIn 2000 2000 axiom ReplSepE_impred: !x:set.!p:set prop.!f:set set.!y:set.y iIn ReplSep x p f -> !P:prop.(!z:set.z iIn x -> p z -> y = f z -> P) -> P lemma !x:set.!y:set.!z:set.!w:set.!u:set.w iIn x -> z = proj1 w -> w = setsum y u -> z = u -> setsum y z iIn x claim !x:set.!y:set.!z:set.z iIn ap x y -> setsum y z iIn x