open Preamble

open Jmeq

open Russell

open Bool

open Nat

open List

open Setoids

open Relations

open Hints_declaration

open Core_notation

open Pts

open Logic

open Types

open Monad

type ('b, 'e) bind_new =
| Bret of 'e
| Bnew of ('b -> ('b, 'e) bind_new)

val bind_new_rect_Type4 :
  ('a2 -> 'a3) -> (('a1 -> ('a1, 'a2) bind_new) -> ('a1 -> 'a3) -> 'a3) ->
  ('a1, 'a2) bind_new -> 'a3

val bind_new_rect_Type3 :
  ('a2 -> 'a3) -> (('a1 -> ('a1, 'a2) bind_new) -> ('a1 -> 'a3) -> 'a3) ->
  ('a1, 'a2) bind_new -> 'a3

val bind_new_rect_Type2 :
  ('a2 -> 'a3) -> (('a1 -> ('a1, 'a2) bind_new) -> ('a1 -> 'a3) -> 'a3) ->
  ('a1, 'a2) bind_new -> 'a3

val bind_new_rect_Type1 :
  ('a2 -> 'a3) -> (('a1 -> ('a1, 'a2) bind_new) -> ('a1 -> 'a3) -> 'a3) ->
  ('a1, 'a2) bind_new -> 'a3

val bind_new_rect_Type0 :
  ('a2 -> 'a3) -> (('a1 -> ('a1, 'a2) bind_new) -> ('a1 -> 'a3) -> 'a3) ->
  ('a1, 'a2) bind_new -> 'a3

val bind_new_inv_rect_Type4 :
  ('a1, 'a2) bind_new -> ('a2 -> __ -> 'a3) -> (('a1 -> ('a1, 'a2) bind_new)
  -> ('a1 -> __ -> 'a3) -> __ -> 'a3) -> 'a3

val bind_new_inv_rect_Type3 :
  ('a1, 'a2) bind_new -> ('a2 -> __ -> 'a3) -> (('a1 -> ('a1, 'a2) bind_new)
  -> ('a1 -> __ -> 'a3) -> __ -> 'a3) -> 'a3

val bind_new_inv_rect_Type2 :
  ('a1, 'a2) bind_new -> ('a2 -> __ -> 'a3) -> (('a1 -> ('a1, 'a2) bind_new)
  -> ('a1 -> __ -> 'a3) -> __ -> 'a3) -> 'a3

val bind_new_inv_rect_Type1 :
  ('a1, 'a2) bind_new -> ('a2 -> __ -> 'a3) -> (('a1 -> ('a1, 'a2) bind_new)
  -> ('a1 -> __ -> 'a3) -> __ -> 'a3) -> 'a3

val bind_new_inv_rect_Type0 :
  ('a1, 'a2) bind_new -> ('a2 -> __ -> 'a3) -> (('a1 -> ('a1, 'a2) bind_new)
  -> ('a1 -> __ -> 'a3) -> __ -> 'a3) -> 'a3

val bind_new_discr : ('a1, 'a2) bind_new -> ('a1, 'a2) bind_new -> __

val bind_new_jmdiscr : ('a1, 'a2) bind_new -> ('a1, 'a2) bind_new -> __

val bnews :
  Nat.nat -> ('a1 List.list -> ('a1, 'a2) bind_new) -> ('a1, 'a2) bind_new

val bnews_strong :
  Nat.nat -> ('a1 List.list -> __ -> ('a1, 'a2) bind_new) -> ('a1, 'a2)
  bind_new

val bbind :
  ('a1, 'a2) bind_new -> ('a2 -> ('a1, 'a3) bind_new) -> ('a1, 'a3) bind_new

val bindNew : Monad.monadProps

open State

val bcompile :
  'a2 Monad.smax_def__o__monad -> ('a2, 'a3) bind_new -> 'a3
  Monad.smax_def__o__monad