proposition: Lemma domPt k v : dom (pts k v : U) =i [pred x | C k & k == x].
proof: Proof. by move=>x; rewrite ptsU domU !inE eq_sym valid_unit dom0; case: eqP. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)