proposition: Lemma big_validV2 (xs : seq I) : valid (\big[PCM.join/Unit]_(i <- xs) f i) -> forall i j, i \In xs -> j \In xs -> i <> j -> valid (f i \+ f j).
proof: Proof. elim: xs=>[|x xs IH] //=; rewrite big_cons. move=>V i j; rewrite !InE; case=>[->|Xi][->|Xj] N //; last first. - by apply: IH=>//; apply: (validR V). - by rewrite joinC; apply: (big_validVL V). by apply: (big_validVL V)=>// /esym. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq bigop fintype finset) pcm(options axioms prelude seqperm pred seqext)