proposition: Lemma omapVUn a f1 f2 : omap a (f1 \+ f2) = if valid (f1 \+ f2) then omap a f1 \+ omap a f2 else um_undef.
proof: Proof. case: ifP; first by apply: omapUn. by move/negbT/invalidE=>->; 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)