proposition: Lemma valid_omfUn f1 f2 h1 h2 : valid (h1 \+ h2) -> valid (f1 h1 \+ f2 h2).
proof: Proof. case: f1=>s1 [m1 H1]; case: f2=>s2 [m2 H2] /= V. rewrite H1 H2 validUnAE !valid_omap // (validL V) (validR V) /=. apply/allP=>x /dom_omap_sub D2; apply/negP=>/dom_omap_sub. by move/(dom_inNL V); rewrite D2. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)