proposition: Lemma comp_omf_ax : OmapFun.axiom (f2 \o f1) (fun x => obind (fun v=> map_fun f2 (x.1, v)) (map_fun f1 x)).
proof: Proof. case: f1=>s1 [m1 H1]; case: f2=>s2 [m2 H2] x /=. by rewrite H1 H2 omap_comp. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)