This required a new ectx axiom: Positivity of evaluation contexts. This axiom was
also present in the old Iris 1.1 development, back when it still derived lifting
axioms for ectx languages.

Also remove some superfluous map_ prefixes.

They will use Iris is a library, in that paper's repo

The proof is not pretty, though...

Thanks to Amin Timany for the suggestion.

add a version of [cancel] that works with goals of the form [_ |- pvs _]; and use that for the barrier proof

This cleans up some ad-hoc stuff and prepares for a generalization
of saved propositions.

And now the part that I forgot to commit.

Now that there is more of it, it deserves its own place :).

start the heap construction: load from a heap is done... store, CAS, and singleton (mapsto) to be done