proposition: Lemma vrf_dealloc A (v : A) j (Q : post unit) : (x \notin dom j -> valid j -> Q (Val tt) j) -> vrf (x :-> v \+ j) dealloc Q.
proof: Proof. move=>H Vi /=. have J: x :-> v \+ j \In dealloc_pre. - by rewrite /dealloc_pre -toPredE /= domPtUnE. exists J=>_ _ [->-> Hx]. rewrite freePtUn //; apply: H; last by exact: (validR Vi). by move: Hx; rewrite domPtUnE validPtUn; case/and3P. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude) pcm(pcm unionmap heap) htt(domain)