const binunion : set set set const Empty : set axiom binunion_idl: !x:set.binunion Empty x = x axiom binunion_com: !x:set.!y:set.binunion x y = binunion y x claim !x:set.binunion x Empty = x