module email sig Name, Addr {} assert A { all friends, spammers: set Name, addr: Name -> Addr | (friends - spammers).addr = friends.addr - spammers.addr } check A for 2