proposition: Lemma big_size_dom (xs : seq I) : valid (\big[PCM.join/Unit]_(i <- xs) f i) -> size (dom (\big[PCM.join/Unit]_(i <- xs) f i)) = \sum_(i <- xs) (size (dom (f i))).
proof: Proof. elim: xs=>[|x xs IH] /=; first by rewrite !big_nil dom0. rewrite !big_cons=>V; rewrite size_domUn //; congr (size _ + _). by apply/IH/(validR V). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)