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