proposition: Lemma big_validV (xs : seq I) i : valid (\big[PCM.join/Unit]_(i <- xs) f i) -> i \In xs -> valid (f i).
proof: Proof. elim: xs=>[|x xs IH] in i * => //. rewrite big_cons InE=>V [->|]; first by apply: (validL V). by apply: IH; rewrite (validR V). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq bigop fintype finset) pcm(options axioms prelude seqperm pred seqext)