proposition: Lemma bnd_deallocR e (v : A) x i (f : forall k, form k i) (r : post B) : vrf (f Unit) (e tt) r -> vrf (f (x :-> v)) (bind (dealloc x) e) r.
proof: Proof. by move=>H; apply/vrf_bind/val_deallocR. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat eqtype seq ssrfun) pcm(options axioms pred prelude) pcm(pcm autopcm unionmap heap) htt(model)