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