proposition: Lemma umpreimUn p f1 f2 : valid (f1 \+ f2) -> um_preim p (f1 \+ f2) =1 predU (um_preim p f1) (um_preim p f2).
proof: Proof. move=>v x; rewrite /um_preim findUnL //=. case X: (find x f1)=>[a|]; case Y: (find x f2)=>[b|] /=. - by move: (dom_inNL v (find_some X)); rewrite (find_some Y). - by rewrite ifT ?(find_some X) // orbC. - by rewrite ifN //; apply/find_none. by rewrite ifN //; apply/find_none. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)