proposition: Lemma umfiltk_dom f1 f2 : valid (f1 \+ f2) -> um_filterk (mem (dom f1)) (f1 \+ f2) = f1.
proof: Proof. move=>W; apply/umem_eq; first by rewrite valid_umfilt. - by rewrite (validL W). case=>k v; rewrite In_umfilt; split=>[|H]. - by case=>H /InUn [] // /In_dom; rewrite (negbTE (dom_inNL W H)). by split; [apply: In_dom H | apply: InL]. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)