proposition: Lemma readP : Model.conseq (Model.read_s A x) [read_s].
proof: Proof. move=>i H D; split=>[|{H D} y _ [->] H _ i1 h E1 D E2]. - case: H D=>i1 [i2][->][[v]] -> _ D /=. rewrite domPtUn inE /= D eq_refl; split=>//. by exists v; rewrite lookPtUn. move: E1 E2 H D=>-> [v ->] H D; exists (x :-> v); do 3!split=>//. move=>w; move/(pts_inj (defUnl D))=><-; apply: H. by rewrite lookPtUn. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat ssrfun seq eqtype) LemmaOverloading(heaps rels hprop stmod)