proposition: Lemma subheap_def h1 h2 : subheap h1 h2 -> def h1 /\ def h2.
proof: Proof. by case=>[subdm _]; move/andP: (subdom_def subdm). Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep