proposition: Lemma bindP : Model.conseq (Model.bind_s [s1] (fr \o s2)) [bind_s].
proof: Proof. move=>i H D; split=>[|{H D}]. - case: H D=>i1 [i2][->][[H S]] _ D. split=>[|y m]; first by apply: fr_pre. by case/(locality D H)=>m1 [->][_]; move/S; apply: fr_pre. move=>y m H _ i1 i2 E D1 [H1 S1]; rewrite {i}E in H D1 *. case: H=>[[x][h][]|[e][->]]; case/(locality D1 H1)=>h1 [->][D2] T2. - move/S1: (T2)=>H2; case/(locality D2 H2)=>m1 [->][D3] T3. by exists m1; do !split=>//; left; exists x; exists h1. by exists h1; do !split=>//; right; exists e. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat ssrfun seq eqtype) LemmaOverloading(heaps rels hprop stmod)