val bind_div_st_req (#a: Type) (wp: pure_wp a) (req_g: (a -> Type0)) : Type0
let bind_div_st_req (#a:Type) (wp:pure_wp a)
                    (req_g:a -> Type0)
  : Type0
  = FStar.Monotonic.Pure.elim_pure_wp_monotonicity wp;
    wp (fun _ -> True) /\ (forall x. req_g x)
val bind_div_st_req (#a: Type) (wp: pure_wp a) (req_g: (a -> Type0)) : Type0
let bind_div_st_req (#a: Type) (wp: pure_wp a) (req_g: (a -> Type0)) : Type0 =
FStar.Monotonic.Pure.elim_pure_wp_monotonicity wp;
wp (fun _ -> True) /\ (forall x. req_g x)
Steel.ST.Coercions.fst.checked
Steel.ST.Effect.Ghost.fst.checked Steel.ST.Effect.Ghost.fst.checked Steel.ST.Effect.AtomicAndGhost.fst.checked Steel.ST.Effect.AtomicAndGhost.fst.checked Steel.ST.Effect.Atomic.fst.checked Steel.ST.Effect.Atomic.fst.checked Steel.ST.Effect.fst.checked Steel.ST.Effect.fst.checked Steel.Memory.fsti.checked Steel.Effect.Atomic.fst.checked Steel.Effect.Atomic.fst.checked Steel.Effect.fst.checked Steel.Effect.fst.checked prims.fst.checked FStar.Universe.fsti.checked FStar.Pervasives.fsti.checked FStar.Monotonic.Pure.fst.checked FStar.Ghost.fsti.checked
Steel.ST.Coercions.fst
Prims.pure_wp Prims.l_and Prims.l_True Prims.l_Forall Prims.unit FStar.Monotonic.Pure.elim_pure_wp_monotonicity
(*
   Copyright 2020 Microsoft Research

   Licensed under the Apache License, Version 2.0 (the "License");
   you may not use this file except in compliance with the License.
   You may obtain a copy of the License at

       http://www.apache.org/licenses/LICENSE-2.0

   Unless required by applicable law or agreed to in writing, software
   distributed under the License is distributed on an "AS IS" BASIS,
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
   See the License for the specific language governing permissions and
   limitations under the License.
*)
module Steel.ST.Coercions
(** This module aggregates several of the core effects and utilities
    associated with the Steel.ST namespace.

    Client modules should typically just [open Steel.ST.Util] and
    that should bring most of what they need in scope.
*)
open FStar.Ghost
open Steel.Memory
open Steel.ST.Effect.Ghost
module U = FStar.Universe

module SF = Steel.Effect
module SA = Steel.Effect.Atomic

module STF = Steel.ST.Effect
module STG = Steel.ST.Effect.Ghost
module STA = Steel.ST.Effect.Atomic
module STAG = Steel.ST.Effect.AtomicAndGhost

friend Steel.ST.Effect.AtomicAndGhost
friend Steel.Effect.Atomic
friend Steel.Effect
friend Steel.ST.Effect
friend Steel.ST.Effect.Ghost
friend Steel.ST.Effect.Atomic

unfold
let bind_div_st_req (#a:Type) (wp:pure_wp a)
                    (req_g:a -> Type0)
val bind_div_st_req (#a: Type) (wp: pure_wp a) (req_g: (a -> Type0)) : Type0
wp: Prims.pure_wp a -> req_g: (_: a -> Type0) -> Type0