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