proposition: Lemma bnd_deallocR s (v : A) x h1 h2 (f : Update h1 h2 empty (x:->v)) (r : cont B) : verify (s tt) h1 r -> verify (bind_s (dealloc_s x) s) h2 r.
proof: Proof. set l := rest f. have H1 : h1 = empty :+ l by eapply (update1 f). have H2 : h2 = (x :-> v) :+ l by eapply (update2 f). by rewrite H1 H2 un0h; apply bnd_dealloc. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun) LemmaOverloading(heaps stmod stsep stlog)