proposition: Lemma umfiltk_preimUn (q : pred V) f1 f2 : valid (f1 \+ f2) -> um_filterk (um_preim q (f1 \+ f2)) f1 = um_filterk (um_preim q f1) f1.
proof: Proof. move=>v; apply: eq_in_umfiltk; move=>x xf1; rewrite umpreimUn // inE orbC. have -> : um_preim q f2 x = false=>//. by move: (dom_inNL v xf1); rewrite /um_preim; case: dom_find=>//->. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)