proposition: Lemma bigInX (xs : seq I) a v : (a, v) \In \big[PCM.join/Unit]_(i <- xs) f i -> exists2 i, i \In xs & (a, v) \In f i.
proof: Proof. by case/In_find/big_find_someX=>x X /In_find; exists x. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)