proposition: Lemma subheapUnl h1 h2 : def (h1 :+ h2) -> subheap h1 (h1 :+ h2).
proof: Proof. move=>D; rewrite -{1}[h1]unh0; apply: subheapUn=>//. - by apply: subheap_refl; apply: defUnl D. by apply: subheapE; apply: defUnr D. Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep