proposition: Lemma defE h : reflect (def h /\ forall x, x \notin dom h)(empb h).
proof: Proof. case: empP=>T; constructor; first by rewrite T. case=>D E; case: T; case: h D E=>// f H _; rewrite /dom => E. apply/heapE; apply/supp_nilE. by case: (supp f) E=>// x s; move/(_ x); rewrite inE eq_refl. Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep