proposition: Lemma bnd_allocR e (v : A) i (r : post B) : (forall x, vrf (x :-> v \+ i) (e x) r) -> vrf i (bind (alloc v) e) r.
proof: Proof. by move=>H; apply/vrf_bind/val_allocR. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat eqtype seq ssrfun) pcm(options axioms pred prelude) pcm(pcm autopcm unionmap heap) htt(model)