proposition: Lemma umpleq_dom k v f : valid f -> [pcm pts k v <= f] -> k \in dom f.
proof: Proof. by move=>W [z E]; subst f; rewrite domPtUn inE W eq_refl. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)