fact: Definition dealloc_s : spec unit := (fun i => exists A : Type, exists v:A, i = x :-> v, fun y i m => y = Val tt /\ m = empty).
imports: mathcomp(ssreflect ssrbool ssrnat ssrfun seq eqtype) LemmaOverloading(heaps rels hprop stmod)