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