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