proposition: Lemma big_domUn (xs : seq I) : dom (\big[PCM.join/Unit]_(i <- xs) f i) =i [pred x | valid (\big[PCM.join/Unit]_(i <- xs) f i) & has (fun i => x \in dom (f i)) xs].
proof: Proof. elim: xs=>[|x xs IH] i; first by rewrite big_nil inE /= dom0 valid_unit. rewrite big_cons /= inE domUn inE IH inE /=. by case V : (valid _)=>//=; rewrite (validR V) /=. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)