proposition: Lemma big_validV2I (xs : seq I) : Uniq xs -> (forall i, i \In xs -> valid (f i)) -> (forall i j, i \In xs -> j \In xs -> i <> j -> valid (f i \+ f j)) -> valid (\big[PCM.join/Unit]_(i <- xs) f i).
proof: Proof. elim: xs=>[|x xs IH] /=; first by rewrite big_nil valid_unit. case=>X Uq H1 H2; rewrite big_cons validUnAE. rewrite H1 /=; last by rewrite InE; left. rewrite IH //=; last first. - by move=>i j Xi Xj; apply: H2; rewrite InE; right. - by move=>i Xi; apply: H1; rewrite InE; right. apply/allP=>a /=; apply: contraL=>Dx; apply/negP. rewrite big_domUn inE=>/andP [V] /hasPIn [y Y Dy]. have : x <> y by move=>N; rewrite N in X; move/X: Y. move/(H2 x y (or_introl erefl) (or_intror Y)). by case: validUn=>// _ _ /(_ a Dx); rewrite Dy. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)