proposition: Lemma freeUnV k f1 f2 : valid (f1 \+ f2) -> free (f1 \+ f2) k = free f1 k \+ free f2 k.
proof: Proof. move=>V'; rewrite freeUn domUn V' /=; case: ifP=>//. by move/negbT; rewrite negb_or; case/andP=>H1 H2; rewrite !dom_free. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)