proposition: Lemma val_deallocR (v : A) x i (f : forall k, form k i) (r : post unit) : (valid (untag (f Unit)) -> r (Val tt) (f Unit)) -> vrf (f (x :-> v)) (dealloc x) r.
proof: Proof. by rewrite !formE unitL=>H; apply: vrf_dealloc. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat eqtype seq ssrfun) pcm(options axioms pred prelude) pcm(pcm autopcm unionmap heap) htt(model)