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