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