proposition: Lemma omapUn a f1 f2 : valid (f1 \+ f2) -> omap a (f1 \+ f2) = omap a f1 \+ omap a f2.
proof: Proof. move=>W; rewrite /omap W (validL W) (validR W); set b := fun z kv => _. have H x y kv : b (x \+ y) kv = b x kv \+ y. - by rewrite /b; case: (a kv)=>// z; rewrite joinAC. rewrite (foldl_perm H _ (assocs_perm W)) foldl_cat. by rewrite joinC -(foldl_init H) unitL. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)