proposition: Lemma try_writeR e1 e2 (v : A) (w : B) x i (f : forall k, form k i) (r : post C) : vrf (f (x :-> v)) (e1 tt) r -> vrf (f (x :-> w)) (try (write x v) e1 e2) r.
proof: Proof. by move=>H; apply/vrf_try/val_writeR. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat eqtype seq ssrfun) pcm(options axioms pred prelude) pcm(pcm autopcm unionmap heap) htt(model)