proposition: Lemma dealloc_dstrict : def_strict dealloc_sp.
proof: Proof. case=>p H y [h][/=]; case/H=>_ H1 [H2][H3] H4. suff: def (free x h) by rewrite -H4. by rewrite defF. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) LemmaOverloading(prelude heaps rels hprop domains)