proposition: Lemma vrf_allocb i (Q : post ptr) : (forall x, valid (updi x (nseq n v) \+ i) -> Q (Val x) (updi x (nseq n v) \+ i)) -> vrf i allocb Q.
proof: Proof. move=>H Vi /=. exists I=>_ _ [l][->-> V]. by apply: H. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude) pcm(pcm unionmap heap) htt(domain)