Rename mapsto_mapsto_ne and add easier-to-use variant
This is factored out of !558 (merged); so far we were unable to agree on good names for these two lemmas.
This is factored out of !558 (merged); so far we were unable to agree on good names for these two lemmas.