module email
sig Target {}
part sig Addr, Name extends Target {}
part sig Alias, Group extends Name {}
sig AddrBook {
	map: Name -> Target
	}
fact {all b: AddrBook | no n: Name | n in n.^(b.map)}
fun add (b, b': AddrBook, n: Name, a: Addr) {b'.map = b.map + n->a}
fun lookup (b: AddrBook, n: Name): set Addr {
	result = n.^(b.map) & Addr }
assert addLocal {all b,b': AddrBook, n,n': Name, a: Addr |
	add (b,b',n,a) and n != n' => lookup (b,n') = lookup (b',n') }
check addLocal for 3 but 2 AddrBook