proposition: Lemma freeUnL k f1 f2 : k \notin dom f1 -> free (f1 \+ f2) k = f1 \+ free f2 k.
proof: Proof. move=>V1; rewrite freeUn domUn inE (negbTE V1) /=. case: ifP; first by case/andP; rewrite dom_free. move/negbT; rewrite negb_and; case/orP=>V2; last by rewrite dom_free. suff: ~~ valid (f1 \+ free f2 k) by move/invalidE: V2=>-> /invalidE ->. apply: contra V2; case: validUn=>// H1 H2 H _. case: validUn=>//; first by rewrite H1. - by move: H2; rewrite validF => ->. move=>x H3; move: (H _ H3); rewrite domF inE /=. by case: ifP H3 V1=>[|_ _ _]; [move/eqP=><- -> | move/negbTE=>->]. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)