proposition: Lemma omapUn_some (a : K * V -> option V') f1 f2 : (forall x, x \In f1 -> a x) -> (forall x, x \In f2 -> a x) -> omap a (f1 \+ f2) = omap a f1 \+ omap a f2.
proof: Proof. move=>H1 H2; have Ev : valid (omap a f1 \+ omap a f2) = valid (f1 \+ f2). - by rewrite !validUnAE !valid_omap // !dom_omap_some. case W : (valid (f1 \+ f2)); first by rewrite omapUn. move: W (W); rewrite -{1}Ev=>/negbT/invalidE -> /negbT/invalidE ->. by rewrite omap_undef. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)