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