module sets
sig X {}
sig Set {elts: set X}
fact {
	all s: Set, e: X |
		some s': Set | s'.elts = s.elts + e
	}
assert A {
	all a, b: Set | some c: Set | c.elts = a.elts + b.elts
	}
check A