proposition: Lemma writeP : Model.conseq (Model.write_s x v) [write_s].
proof: Proof. move=>i H D; split=>[|{H D} y m [->] <- D1 i1 h E1 D2 [B][w] E2]. - case: H D=>i1 [i2][->][[B]][y] -> _ D /=. by rewrite domPtUn inE /= D eq_refl. move: E1 E2 D1 D2=>->->-> D; exists (x :-> v). by rewrite updUnl domPt inE /= eq_refl (defPt_null D) /= updU eq_refl. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat ssrfun seq eqtype) LemmaOverloading(heaps rels hprop stmod)