proposition: Lemma dealloc_coherent : coherent dealloc_sp.
proof: Proof. move=>p y m; split. - by case=>i [H1][->][H2] ->; exists i; exists H1; exists i. by case=>i [H1][_][<-][->][H2] ->; exists i. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) LemmaOverloading(prelude heaps rels hprop domains)