proposition: Lemma updPtUnO A1 A2 x i (v1 : A1) (v2 : A2) (f : forall k, partition k i) : upd x (idyn v2) (untag (f (x :-> v1))) = f (x :-> v2).
proof: Proof. by rewrite !partitionE; apply: updPtUn. Qed.
imports: Coq(ssreflect ssrbool ssrfun Eqdep) mathcomp(ssrnat eqtype seq path) pcm(options axioms finmap) pcm(pcm unionmap)