fact: Definition free x h : heap := (if h is Def hs ns then Def (free_nullP x ns) else Undef).
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep