proposition: Lemma big_valid_dom_seq (xs : seq I) : (valid (\big[PCM.join/Unit]_(i <- xs) g i) = all (fun i => valid (g i)) xs && uniq (\big[cat/[::]]_(i <- xs) dom (g i))) * (dom (\big[PCM.join/Unit]_(i <- xs) g i) =i if valid (\big[PCM.join/Unit]_(i <- xs) g i) then \big[cat/[::]]_(i <- xs) dom (g i) else [::]).
proof: Proof. elim: xs=>[|x xs [IH1 IH2]]; first by rewrite !big_nil valid_unit /= dom0. rewrite !big_cons cat_uniq /=; split=>[|z]; last first. - rewrite domUn inE; case V : (valid _)=>//=. by rewrite mem_cat IH2 (validR V). rewrite validUnAE IH1 -all_predC -!andbA uniq_dom /=. case V : (valid (g x))=>//=; case A : (all _)=>//=. rewrite [RHS]andbC; case Uq : (uniq _)=>//=. by apply: eq_all_r=>i; rewrite IH2 IH1 A Uq. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)