proposition: Lemma allocb_has_spec : allocb_sp \In has_spec allocb_s.
proof: Proof. by move=>i y m [[/= H D]][_][<-][->] ->; exists (fresh i). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) LemmaOverloading(prelude heaps rels hprop domains)