proposition: Lemma dom_free k f : k \notin dom f -> free f k = f.
proof: Proof. rewrite -{3}[f]UMC.tfE !umEX /UM.dom /UM.free. by case: (UMC.from f)=>[|f' H] //; apply: rem_supp. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)