proposition: Lemma umpleq_subdom x y : valid y -> [pcm x <= y] -> {subset dom x <= dom y}.
proof: Proof. by move=>W H; case: H W=>a -> W b D; rewrite domUn inE W D. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)