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