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