proposition: Lemma subdom_umpleq a (x y : U) : valid (x \+ y) -> [pcm a <= x \+ y] -> {subset dom a <= dom x} -> [pcm a <= x].
proof: Proof. move=>W H Sx; move: (umpleq_filtk_meet Sx H); rewrite umfiltUn //. rewrite umfiltk_memdomE; move/subset_disjC: (valid_subdom W). by move/(subdom_umfiltk0 _ (validR W))=>->; rewrite unitR. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)