proposition: Lemma omapv_comp (f : U1) : omapv a2 (omapv a1 f : U2) = omapv (obind a2 \o a1) f :> U3.
proof: Proof. by apply: omap_comp. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)