fact: Definition to (b : base) : heap := if b is UM.Def hs ns then Def (base_heap ns) else Undef.
imports: Coq(ssreflect ssrbool ssrfun Eqdep) mathcomp(ssrnat eqtype seq path) pcm(options axioms finmap) pcm(pcm unionmap)