proposition: Lemma subheapE h : def h -> subheap empty h.
proof: Proof. by split; [apply subdom_emp | rewrite dom0]. Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep