const proj0 : set set const setsum : set set set axiom proj0_pair_eq: !x:set.!y:set.proj0 (setsum x y) = x const ap : set set set const Empty : set axiom proj0_ap_0: !x:set.proj0 x = ap x Empty claim !x:set.!y:set.ap (setsum x y) Empty = x