proposition: Lemma tryP : Model.conseq (Model.try_s [s] (fr \o s1) (fr \o s2)) [try_s].
proof: Proof. move=>i H D; split=>[|{H D} y m H1 D1 i1 h E1 D2 /= [H2][H3] H4]. - case: H D=>i1 [i2][->][[H [S1 S2]]] _ D. split; first by apply: fr_pre. split=>y m; case/(locality D H)=>m1 [->][_]; [move/S1 | move/S2]; by apply: fr_pre. rewrite {i}E1 /= in H1 D2. case: H1=>[[x]|[x]][h1][]; case/(locality D2 H2)=>m1 [->][D3] T1; move: (T1); [move/H3 | move/H4]=>T'; case/(locality D3 T')=>m2 [->][D4] T2; exists m2; do 2!split=>//; [left | right]; by exists x; exists m1. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat ssrfun seq eqtype) LemmaOverloading(heaps rels hprop stmod)