proposition: Lemma try_read s1 s2 v x i (r : cont B) : verify (s1 v) (x :-> v :+ i) r -> verify (try_s (read_s A x) s1 s2) (x :-> v :+ i) r.
proof: Proof. move=>*; apply: try_do; first by [exists v]; by move=>y m [<-]; move/(_ v (erefl _))=>// [->]. Qed.
imports: mathcomp(ssreflect ssrbool seq ssrfun) LemmaOverloading(heaps rels hprop stmod stsep)