proposition: Lemma bnd_readR s v x i (f : update (x :-> v) i) (r : cont B) : verify (s v) f r -> verify (bind_s (read_s A x) s) f r.
proof: Proof. by rewrite updateE; apply: bnd_read. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun) LemmaOverloading(heaps rels stmod stsep stlog)