proposition: Lemma valid_omapUn a1 a2 f1 f2 : valid (f1 \+ f2) -> valid (omap a1 f1 \+ omap a2 f2).
proof: Proof. move=>W; rewrite validUnAE !valid_omap // (validL W) (validR W) /=. apply/allP=>z /In_dom_omap [] //= x1 [w1][/In_dom /= D1 _]. apply/negP=>/In_dom_omap [] //= x2 [w2][/In_dom /=]. by move/(dom_inNR W)/negbTE: D1=>->. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)