proposition: Lemma omap_morph_ax a : morph_axiom (@sepT _) (omap a).
proof: Proof. split=>[|x y W _]; first by rewrite omap0. by rewrite -omapUn // valid_omap. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)