proposition: Lemma dom_free h x : x \notin dom h -> free x h = h.
proof: Proof. by case: h=>[|h H] // E; apply/heapE; apply: rem_supp. Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep