proposition: Lemma size_domUn f1 f2 : valid (f1 \+ f2) -> size (dom (f1 \+ f2)) = size (dom f1) + size (dom f2).
proof: Proof. by move/perm_domUn/seq.perm_size; rewrite size_cat. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)