proposition: Lemma alloc_has_spec : alloc_sp \In has_spec alloc_s.
proof: Proof. move=>i y m [[/= H D]][_][<-][l][->][->][H1] H2. exists l; do !split=>//. rewrite (_ : i = i :+ empty); last by rewrite unh0. by rewrite updUnl (negbTE H2) unh0. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) LemmaOverloading(prelude heaps rels hprop domains)