proposition: Lemma free0 x : free x empty = empty.
proof: Proof. by apply/heapE; rewrite rem_empty. Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep