proposition: Lemma big_domUnE (xs : seq I) a : valid (\big[PCM.join/Unit]_(i <- xs) f i) -> a \in dom (\big[PCM.join/Unit]_(i <- xs) f i) = has (fun i => a \in dom (f i)) xs.
proof: Proof. by move=>V; rewrite big_domUn inE V. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)