proposition: Lemma bnd_doR (s : spec A) s2 i j (f : forall k, update k j) (r : cont B) : s.1 i -> (forall x m, s.2 (Val x) i m -> verify (s2 x) (f m) r) -> (forall e m, s.2 (Exn e) i m -> def (f m) -> r (Exn e) (f m)) -> verify (bind_s s s2) (f i) r.
proof: Proof. move=>H1 H2 H3; rewrite updateE; apply: (bnd_do H1). - by move=>x m; move: (H2 x m); rewrite updateE. by move=>x m; move: (H3 x m); rewrite updateE. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun) LemmaOverloading(heaps rels stmod stsep stlog)