proposition: Lemma dealloc_has_spec : dealloc_sp \In has_spec dealloc_s.
proof: Proof. by move=>i y m [[/= H1 D1]][_][<-][->][H2] ->. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) LemmaOverloading(prelude heaps rels hprop domains)