Add mapsto_ne helper lemma

Here's one case this lemma might be useful. Suppose you want to programmatically generate namespaces for e.g. locks:

Definition lockN (l : loc) := nroot .@ "lock" .@ l.

Then to know that two such namespaces are disjoint, we need to know that the corresponding locations are distinct.