proposition: Lemma cancelTO A1 A2 h1 h2 x (v1 : A1) (v2 : A2) (f1 : partition (x :-> v1) h1) (f2 : partition (x :-> v2) h2) : valid (untag f1) -> f1 = f2 :> heap -> A1 = A2.
proof: Proof. by rewrite !partitionE; apply: hcancelT. Qed.
imports: Coq(ssreflect ssrbool ssrfun Eqdep) mathcomp(ssrnat eqtype seq path) pcm(options axioms finmap) pcm(pcm unionmap)