proposition: Lemma dom_omapUn (a : K*V -> option V') f1 f2 : dom (omap a (f1 \+ f2)) =i [pred x | valid (f1 \+ f2) & (x \in dom (omap a f1)) || (x \in dom (omap a f2))].
proof: Proof. move=>x; case W: (valid (f1 \+ f2)); last first. - by move/negbT/invalidE: W=>->; rewrite omap_undef dom_undef. by rewrite omapUn // domUn !inE -omapUn // valid_omap // W. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)