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