proposition: Lemma bnd_do (s : spec A) s2 i j (r : cont B) : s.1 i -> (forall x m, s.2 (Val x) i m -> verify (s2 x) (m :+ j) r) -> (forall e m, s.2 (Exn e) i m -> def (m :+ j) -> r (Exn e) (m :+ j)) -> verify (bind_s s s2) (i :+ j) r.
proof: Proof. move=>H1 H2 H3; apply: bnd_is_try. apply: try_do=>// e m H4; apply: frame0; apply: frame1=>_. by split=>// y m1 [->] -> _; rewrite un0h; apply: H3. Qed.
imports: mathcomp(ssreflect ssrbool seq ssrfun) LemmaOverloading(heaps rels hprop stmod stsep)