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