proposition: Lemma bnd_is_try (A B : Type) (s1 : spec A) (s2 : A -> spec B) i r : verify (try_s s1 s2 (fun y => fr (throw_s B y))) i r -> verify (bind_s s1 s2) i r.
proof: Proof. move=>H; apply: frame0=>D. case: {H D} (H D) (D)=>[[i1]][i2][->][[H1 [H2 H3]]] _ T D. split=>[|y m]. - split=>[|x m]; first by apply: fr_pre H1. by case/(locality D H1)=>m1 [->][_]; move/H2; apply: fr_pre. move=>{D} H; apply: T=>h1 h2 E. rewrite {i1 i2 H1 H2 H3}E in H * => D1 [H1][H2] H3. case: H=>[[x][h][]|[e][->]]; move/(locality D1 H1); case=>[m1][->][D2] T1; move: (T1); [move/H2 | move/H3]=>H4. - move=>T2; case/(locality D2 H4): (T2)=>m3 [->][D3]. by exists m3; do !split=>//; left; exists x; exists m1. exists m1; do !split=>//; right; exists e; exists m1; split=>//. move=>j1 j2 E D _; rewrite {m1 D2}E in T1 D H4 *. exists j1; do !split=>//; move=>k1 k2 -> D2 ->. by exists empty; rewrite un0h; do !split=>//; apply: defUnr D2. Qed.
imports: mathcomp(ssreflect ssrbool seq ssrfun) LemmaOverloading(heaps rels hprop stmod stsep)