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.