fact: Definition dealloc_sp (p : ideald dealloc_s.1) (y : ans unit) m := exists i, i \In id_val p /\ y = Val tt /\ x \in dom i /\ m = free x i.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) LemmaOverloading(prelude heaps rels hprop domains)