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