proposition: Lemma empP h : reflect (h = empty) (empb h).
proof: Proof. case: h=>[|h] /=; first by right. case: eqP=>E H; first by apply: ReflectT; apply/heapE; apply/supp_nilE. by apply: ReflectF; move/heapE=>S; rewrite S supp_nil in E. Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep