proposition: Lemma alloc_dstrict : def_strict alloc_sp.
proof: Proof. case=>p H y [m][/= H1][l][H2][H3][H4] H5; case/H: H1=>_ D. suff {H3}: def (m :+ l :-> v) by rewrite -H3. by rewrite unC defPtUn H4 D H5. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) LemmaOverloading(prelude heaps rels hprop domains)