proposition: Lemma try_writeR s1 s2 (v : A) (w : C) x i (f : forall k, update k i) (r : cont B) : verify (s1 tt) (f (x :-> v)) r -> verify (try_s (write_s x v) s1 s2) (f (x :-> w)) r.
proof: Proof. rewrite !updateE; apply: try_write. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun) LemmaOverloading(heaps rels stmod stsep stlog)