fact: Parameter vrf_ret : forall A x i (Q : post A), (valid i -> Q (Val x) i) -> vrf i (ret x) Q.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude) pcm(pcm unionmap heap) htt(domain)