Mapsto notation changes: remove `l ↦ -`, and change `l ↦□ I` to `l ↦_I □`.

The l ↦ - and l ↦{q} - notations are not used much (<10 uses across all reverse dependencies), and they are rather confusing when parsing statements like ``l ↦ - ∗ P`, which looks as if there was a magic wand here. So @robbertkrebbers and me agreed we should just kill it.

Furthermore, the attractive ↦□ notation is currently used by gen_inv_heap but we'd like to use them for the persistent points-to that @simonfv is working on. So change it to l ↦_I □. This can still be potentially confusing though, such as l ↦_I □ ∗ P -- but at least □∗ is not a connective that makes any sense, so I think this is better than l ↦_I - ∗ P. An alternative might be l ↦_I ∗ P, but @robbertkrebbers did not like this much.