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