proposition: Lemma bnd_allocb s (v : A) n i (r : cont B) : (forall x, verify (s x) (updi x (nseq n v) :+ i) r) -> verify (bind_s (allocb_s v n) s) i r.
proof: Proof. by move=>*; apply: bnd_is_try; apply: try_allocb. Qed.
imports: mathcomp(ssreflect ssrbool seq ssrfun) LemmaOverloading(heaps rels hprop stmod stsep)