proposition: Lemma vrf_alloc i (Q : post ptr) : (forall x, valid (x :-> v \+ i) -> Q (Val x) (x :-> v \+ i)) -> vrf i alloc Q.
proof: Proof. move=>H Vi /=. exists I=>_ _ [x][-> -> Hx Hx2]. by apply: H; rewrite validPtUn Hx Vi. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude) pcm(pcm unionmap heap) htt(domain)