proposition: Lemma un0h h : empty :+ h = h.
proof: Proof. by case: h=>[|h H] //; apply/heapE; rewrite fcat0s. Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep