proposition: Lemma bnd_deallocR s (v : B) x i (f : forall k, update k i) (r : cont A) : verify (s tt) (f empty) r -> verify (bind_s (dealloc_s x) s) (f (x :-> v)) r.
proof: Proof. by rewrite !updateE un0h; apply: bnd_dealloc. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun) LemmaOverloading(heaps rels stmod stsep stlog)