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