proposition: Lemma doP : Model.conseq [s1] [s2].
proof: Proof. move=>i H D; split=>[|y m {H D} /=]. - case: H D=>i1 [i2][->][H] _ D. by case: (@pf i1 H (defUnl D))=>H1 _; apply: fr_pre. move=>S D i1 i2 E D2 H2; rewrite {i}E in D S D2 H2. case: (@pf i1 H2 (defUnl D2))=>H1 T1. case: (locality D2 H1 S)=>m1 [->][D3] {S}. by move/T1; move/(_ (defUnl D3))=>T2; exists m1. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat ssrfun seq eqtype) LemmaOverloading(heaps rels hprop stmod)