Variable-Value pairs (i.e., maps) are not retained when one of them gets nullified

Question

I have the following simple model where I try to simulate the nullification of a select Data from a Dataset. Data to Val (d2v) mapping is a field of a signature called Dynamic whose instances correspond to different states of the model (before and after). When I try to simulate this model, I get two unrelated Dynamic instances, even though I explicitly set the d2v mappings of the two Dynamic instances to be the same (except of course the mapping of Data instance being passed to nullify predicate). In other words, the variable-value pairings of the two instances of Dynamic do not match. What am I missing?

sig Data {}
sig Val {}

sig Dynamic {
  d2v: Data -> lone Val,
}

pred nullify [dyn, dyn': Dynamic, d:Data] {
  d in dyn.d2v.univ implies
    dyn'.d2v = dyn.d2v - (d -> d.(dyn.d2v))
  else
     dyn'.d2v = dyn.d2v
}

run nullify for exactly 3 Data,
                exactly 3 Val,
                exactly 2 Dynamic

Here is an example evaluation of the two instances of Dynamic.d2v from Alloy:

sig Dynamic
   Dynamic$0
      field d2v
         Data$2 -> Val$2
   Dynamic$1
      field d2v
         Data$0 -> Val$1
         Data$1 -> Val$0

where Data$2 is the argument of remove predicate. What I would expect, for instance, is the following:

sig Dynamic
   Dynamic$0
      field d2v
         Data$2 -> Val$2
         Data$0 -> Val$1
         Data$1 -> Val$0
   Dynamic$1
      field d2v
         Data$0 -> Val$1
         Data$1 -> Val$0

Answer 1

Are you sure that the instance binds dyn and dyn' to Dynamic$0 and Dynamic$1? It could bind them both to Dynamic$1 for example, satisfying the else arm of your predicate.