proposition: Lemma big_find_someD (xs : seq I) a i v : i \In xs -> a \in dom (f i) -> find a (\big[PCM.join/Unit]_(x <- xs) f x) = Some v -> find a (f i) = Some v.
proof: Proof. elim: xs v=>[|y xs IH] v //=; rewrite big_cons InE. case=>[->|Xi] Da /[dup]/In_find/In_valid V; first by rewrite findUnL // Da. rewrite findUnR // big_domUnE ?(validR V) //=. by rewrite ifT; [apply: IH | apply/hasPIn; exists i]. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)