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