proposition: Lemma bnd_gh1R (r : cont B) : let: Q := fun y i m => forall x, i \In p x -> q x y i m in (i \In p t -> P i) -> (forall x m, q t (Val x) i m -> verify (s1 x) (f m) r) -> (forall e m, q t (Exn e) i m -> def (f m) -> r (Exn e) (f m)) -> i \In p t -> verify (bind_s (P, Q) s1) (f i) r.
proof: Proof. move=>H1 H2 H3; rewrite updateE; apply: (bnd_gh1 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)