proposition: Lemma write_frame : frameable write_prog.
proof: Proof. move=>i j Hx Vij _ _ _ [-> -> _]. exists (upd x (idyn v) i); split=>//; rewrite /write_pre -toPredE /= in Hx. - by rewrite updUnL Hx. by rewrite validUUn. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude) pcm(pcm unionmap heap) htt(domain)