proposition: Lemma val_readR v x i (f : form (x :-> v) i) (r : post A) : (valid (untag f) -> r (Val v) f) -> vrf f (read x) r.
proof: Proof. by rewrite formE; apply: vrf_read. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat eqtype seq ssrfun) pcm(options axioms pred prelude) pcm(pcm autopcm unionmap heap) htt(model)