proposition: Lemma ptsE k (v : dynamic id) : pts k v = to (@UM.pts _ _ _ k v).
proof: Proof. by rewrite /pts /UM.pts /UM.upd /=; case: decP=>// H; rewrite heapE. Qed.
imports: Coq(ssreflect ssrbool ssrfun Eqdep) mathcomp(ssrnat eqtype seq path) pcm(options axioms finmap) pcm(pcm unionmap)