proposition: Lemma omap_predU (a1 a2 : K*V -> option V') f : (forall kv, a1 kv = None \/ a2 kv = None) -> omap a1 f \+ omap a2 f = omap (fun kv => if a1 kv is Some v' then Some v' else if a2 kv is Some v' then Some v' else None) f.
proof: Proof. move=>E; elim/um_indf: f=>[||k v f IH W /(order_path_min (@trans K)) P]. - by rewrite !omap_undef undef_join. - by rewrite !omap0 unitL. rewrite !omapPtUn W /= -IH. case E1 : (a1 (k, v))=>[b1|]; case E2 : (a2 (k, v))=>[b2|] //. - by move: (E (k, v)); rewrite E1 E2; case. - by rewrite joinA. by rewrite joinCA. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)