fact: Definition subheap h1 h2 := subdom h1 h2 /\ forall x, x \in dom h1 -> look x h1 = look x h2.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep