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