fact: Parameter vrf_read : forall A x j (v : A) (Q : post A), (valid (x :-> v \+ j) -> Q (Val v) (x :-> v \+ j)) -> vrf (x :-> v \+ j) (read x) Q.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude) pcm(pcm unionmap heap) htt(domain)