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