proposition: Lemma umpleq_meet a (x y1 y2 : U) : valid (x \+ y1 \+ y2) -> [pcm a <= x \+ y1] -> [pcm a <= x \+ y2] -> [pcm a <= x].
proof: Proof. rewrite um_valid3=> /and3P[V1 V12 V2] H1 H2. apply: subdom_umpleq (V1) (H1) _ => k D. move: {D} (umpleq_subdom V1 H1 D) (umpleq_subdom V2 H2 D). rewrite !domUn !inE V1 V2 /=; case : (k \in dom x)=>//=. by case: validUn V12=>// _ _ L _ /L /negbTE ->. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)