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