val st_wp : a: Type -> Type
let st_wp (a:Type) = wp:st_wp0 a{st_monotonic wp}
module AlgForAll

open FStar.Calc
module FE = FStar.FunctionalExtensionality
module F = FStar.FunctionalExtensionality
module W = FStar.WellFounded
module T = FStar.Tactics.V2
module ID5 = ID5
open Alg

type rwtree a = Alg.tree a [Read; Write]
let tbind : #a:_ -> #b:_ -> rwtree a -> (a -> rwtree b) -> rwtree b = fun c f -> Alg.bind _ _ c f

let st_wp0 (a:Type) : Type = state -> (a & state -> Type0) -> Type0

let st_monotonic #a (w : st_wp0 a) : Type0 =
  //forall s0 p1 p2. (forall r. p1 r ==> p2 r) ==> w s0 p1 ==> w s0 p2
  // ^ this version seems to be less SMT-friendly
  forall s0 p1 p2. (forall x s1. p1 (x, s1) ==> p2 (x, s1)) ==> w s0 p1 ==> w s0 p2
/
prims.fst.checked ID5.fst.checked FStar.WellFounded.fst.checked FStar.Tactics.V2.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Monotonic.Pure.fst.checked FStar.FunctionalExtensionality.fsti.checked FStar.Classical.fsti.checked FStar.Calc.fsti.checked Alg.fst.checked
AlgForAll.fst
a: Type -> Type
AlgForAll.st_wp0 AlgForAll.st_monotonic
let st_wp (a: Type) =
  
wp: st_wp0 a {st_monotonic wp}