proposition: Lemma cancelO A h1 h2 x (v1 v2 : A) (f1 : partition (x :-> v1) h1) (f2 : partition (x :-> v2) h2) : valid (untag f1) -> f1 = f2 :> heap -> [/\ v1 = v2, valid h1 & h1 = h2].
proof: Proof. by rewrite !partitionE; apply: hcancelV. Qed.
imports: Coq(ssreflect ssrbool ssrfun Eqdep) mathcomp(ssrnat eqtype seq path) pcm(options axioms finmap) pcm(pcm unionmap)