proposition: Lemma domUnPt k v f : dom (f \+ pts k v) =i [pred x | valid (f \+ pts k v) & (k == x) || (x \in dom f)].
proof: Proof. by rewrite joinC; apply: domPtUn. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)