proposition: Lemma umpleqk_pleqE a x : valid x -> [pcm a <= x] <-> um_filterk (mem (dom a)) x = a.
proof: Proof. move=>W; split=>[|<-] // H; case: H W=>b ->. by apply: umfiltk_dom. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)