proposition: Lemma vrf_write B (u : B) j (Q : post unit) : (valid (x :-> v \+ j) -> Q (Val tt) (x :-> v \+ j)) -> vrf (x :-> u \+ j) write Q.
proof: Proof. move=>H Vi /=. have J : x :-> u \+ j \In write_pre. - by rewrite /write_pre -toPredE /= domPtUnE. exists J=>_ _ [->-> _]. rewrite updPtUn; apply: H. by rewrite (@validPtUnE _ _ _ _ (idyn u)). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude) pcm(pcm unionmap heap) htt(domain)