proposition: Lemma write_dstrict : def_strict write_prog.
proof: Proof. move=>i Hx _ _ [_ E _]; rewrite /write_pre -toPredE /= in Hx. suff {E}: valid (upd x (idyn v) i) by rewrite -E. by rewrite validU (dom_cond Hx) (dom_valid Hx). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude) pcm(pcm unionmap heap) htt(domain)