const proj1 : set set const setsum : set set set axiom proj1_pair_eq: !x:set.!y:set.proj1 (setsum x y) = y const ap : set set set const ordsucc : set set const Empty : set axiom proj1_ap_1: !x:set.proj1 x = ap x (ordsucc Empty) claim !x:set.!y:set.ap (setsum x y) (ordsucc Empty) = y