proposition: Lemma In_mapv (f : U1) k x : injective a1 -> (k, a1 x) \In (mapv a1 f : U2) <-> (k, x) \In f.
proof: Proof. by move=>G; rewrite In_omapX //=; split; [case=>w H [] /G <-| exists x]. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)