val tbind: #a: _ -> #b: _ -> rwtree a -> (a -> rwtree b) -> rwtree b
val tbind: #a: _ -> #b: _ -> rwtree a -> (a -> rwtree b) -> rwtree b
let tbind : #a:_ -> #b:_ -> rwtree a -> (a -> rwtree b) -> rwtree b = fun c f -> Alg.bind _ _ c f
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
/
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
c: AlgForAll.rwtree a -> f: (_: a -> AlgForAll.rwtree b) -> AlgForAll.rwtree b
AlgForAll.rwtree Alg.bind Prims.Cons Alg.op Alg.Read Alg.Write Prims.Nil
let tbind: #a: _ -> #b: _ -> rwtree a -> (a -> rwtree b) -> rwtree b =
  
fun c f -> Alg.bind _ _ c f