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