proposition: Lemma domF h x : dom (free x h) =i [pred y | if x == y then false else y \in dom h].
proof: Proof. case: h=>[|h H] y /=; rewrite ?inE /=; case: ifP=>// E; by rewrite supp_rem inE /= eq_sym E. Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep