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 const In : set set prop term iIn = In infix iIn 2000 2000 axiom ReplSepI: !x:set.!p:set prop.!f:set set.!y:set.y iIn x -> p y -> f y iIn ReplSep x p f axiom proj1_pair_eq: !x:set.!y:set.proj1 (setsum x y) = y claim !x:set.!y:set.!z:set.setsum y z iIn x -> z iIn ap x y