Here is a constraint for my FatSet example:
where 
and 
are implicitly defined and qualified
as usual. This says that once an integer gets added to my set t it never
disappears. We know this constraint holds because there is no way
to delete elements from the set.
Notice that saying that the cardinality of t always strictly increases:
WRONG! 
is not a constraint for FatSet. It does not hold since taking the union of two sets may not necessarily increase the size of either.