proposition: Lemma val_writeR (v : A) (w : B) x i (f : forall k, form k i) (r : post unit) : (valid (untag (f (x :-> v))) -> r (Val tt) (f (x :-> v))) -> vrf (f (x :-> w)) (write x v) r.
proof: Proof. by rewrite !formE; apply: vrf_write. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat eqtype seq ssrfun) pcm(options axioms pred prelude) pcm(pcm autopcm unionmap heap) htt(model)