Check the equivalence of two approaches to ensuring that all hotel guests get a unique set of keys

Question

[Update] Thanks to @Loïc Gammaitoni for providing the answer. Based on Loïc's insight, this is the model I created to test for equivalence of the two approaches:

sig Key {}

sig Room {
    keys: set Key
}

pred DisjointKeySet_v1 {
    keys in Room lone -> Key
} 

// See page 274 of Software Abstractions.
// It says that this: sig S {f: disj e}
// is equivalent to the constraint:
// all a,b: S | a != b => no a.f & b.f
pred DisjointKeySet_v2 {
    all r, r': Room | r != r' => no  r.keys & r'.keys
} 

assert Equivalent {
    DisjointKeySet_v1  iff DisjointKeySet_v2 
}
check Equivalent

Each guest at a hotel is given a set of keys:

sig Key {}

sig Room {
    keys: set Key
}

We must constrain the sets of keys so that no two guests get an identical key. Here's one approach to implementing that constraint:

fact DisjointKeySet {
    keys in Room lone -> Key
}

A second approach to implementing the constraint involves modifying the declaration of keys:

sig Room {
    keys: disj set Key
}

Are the two approaches equivalent?

I believe they are.

To be certain, I want the Alloy Analyzer to compare the two approaches and search for counterexamples.

How to do this? How to write the proper assert?

Below is an assert that I created. I think that it properly checks for equivalence of the two approaches. Do you agree? My assert seems rather round about. Is there a more direct way of showing equivalence?

sig Key {}

sig Room {
    keys: disj set Key
}

// If each room has a disjoint set of keys,
// then each key may be used with only
// one room
assert Equivalent {
    no k: Key, disj r, r': Room |
        (k in r.keys) and (k in r'.keys)            
}
check Equivalent

Answer 1

The keyword disj is in this context a shorthand for all a, b: Room| a!=b implies no a.keys & b.keys (c.f. Appendix B of Software Abstraction)

To answer your question, you could thus check the assertion:

assert equivalence {
    (keys in Room lone -> Key) <=> (all a, b: Room| a!=b implies no a.keys & b.keys)
}

Results will suggest that both approaches are equivalent.