proposition: Lemma domF k f : dom (free f k) =i [pred x | if k == x then false else x \in dom f].
proof: Proof. rewrite !umEX; case: (UMC.from f)=>[|f' H] x; rewrite inE /=; by case: ifP=>// E; rewrite supp_rem inE /= eq_sym E. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)