Refine_Imperative_HOL.Heapmap_Bench