proposition: Lemma big_find_someX (xs : seq I) a v : find a (\big[PCM.join/Unit]_(i <- xs) f i) = Some v -> exists2 i, i \In xs & find a (f i) = Some v.
proof: Proof. elim: xs=>[|x xs IH]; first by rewrite big_nil find0E. move/[dup]=>E1; rewrite big_cons=>/[dup] E /find_some. rewrite domUn inE=>/andP [V] /orP [] D; last first. - move: E; rewrite findUnR // D=>/IH [j Dj Xj]. by exists j=>//; rewrite InE; right. case/In_domX: D=>w /In_find /[dup] X. move/(big_find_some (dom_valid (find_some E1)) (or_introl erefl)). by rewrite E1; case=>->; exists x=>//; rewrite InE; left. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)