proposition: Lemma subheap_refl h : def h -> subheap h h.
proof: Proof. by move=>D; split=>//; apply: subdom_refl. Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep