Recall our model for a Map given in Dynamics II:

	abstract sig Object {}
	sig Key, Value extends Object {}
	sig Map {
		values: Key -> lone Value
	}

Suppose we want to write a predicate replace(m, m':Map, k:Key, v:Value) for the operation of changing the value associated with an existing Key in a Map. How could we implement this?
	1:
		pred replace(m, m':Map, k:Key, v':Value) { 
			m'.values = m.values + k -> v'
		}
	[2]:
		pred replace(m, m':Map, k:Key, v':Value) { 
			some v:Value | 
				v != v' and k -> v in m.values and m'.values = m.values - k->v + k -> v'
		}

Feedback for wrong answer(1):
This does not work: If there is a Value v != v' s.t. k -> v is in m.values, then m'.values would map both v and v' to k. This is impossible because of the use of lone in the definition of values. 

Feedback for correct answer(2): 
The solution given in 1 does not work: If there is a Value v != v' s.t. k -> v is in m.values, then m'.values would map both v and v' to k. This is impossible because of the use of lone in the definition of values. Removing the existing mapping first avoids this problem.