# define usymIdSet_isUndefined(s) ((s) == usymIdSet_undefined)
/*@iter usymIdSet_elements (sef usymIdSet u, yield usymId el); @*/
# define usymIdSet_isUndefined(s) ((s) == usymIdSet_undefined)
/*@iter usymIdSet_elements (sef usymIdSet u, yield usymId el); @*/