proposition: Lemma domPtUn k v f : dom (pts k v \+ f) =i [pred x | valid (pts k v \+ f) & (k == x) || (x \in dom f)].
proof: Proof. move=>x; rewrite domUn !inE !validPtUn domPt !inE. by rewrite -!andbA; case: (C k). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)