const nat_p : set prop const ordsucc : set set const Empty : set axiom nat_1: nat_p (ordsucc Empty) const setsum : set set set axiom nat_setsum1_ordsucc: !x:set.nat_p x -> setsum (ordsucc Empty) x = ordsucc x claim setsum (ordsucc Empty) (ordsucc Empty) = ordsucc (ordsucc Empty)