proposition: Lemma vrf_read j (v : A) (Q : post A) : (valid (x :-> v \+ j) -> Q (Val v) (x :-> v \+ j)) -> vrf (x :-> v \+ j) read Q.
proof: Proof. move=>H Vi /=. have J : x :-> v \+ j \In read_pre. - split; first by rewrite domPtUnE. by exists v; rewrite findPtUn. exists J=>_ _ [w [->->]]. rewrite findPtUn //; case=>/inj_pair2 {w}<-. by apply: H. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude) pcm(pcm unionmap heap) htt(domain)