open Preamble

open State

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

open Bind_new

type ('b, 'e) bind_list = ('b, 'e List.list) Bind_new.bind_new

(** val dpi1__o__blist_from_list__o__inject :
    ('a2 List.list, 'a3) Types.dPair -> ('a1, 'a2 List.list)
    Bind_new.bind_new Types.sig0 **)
let dpi1__o__blist_from_list__o__inject x4 =
  Bind_new.Bret x4.Types.dpi1

(** val eject__o__blist_from_list__o__inject :
    'a2 List.list Types.sig0 -> ('a1, 'a2 List.list) Bind_new.bind_new
    Types.sig0 **)
let eject__o__blist_from_list__o__inject x4 =
  Bind_new.Bret (Types.pi1 x4)

(** val blist_from_list__o__inject :
    'a2 List.list -> ('a1, 'a2 List.list) Bind_new.bind_new Types.sig0 **)
let blist_from_list__o__inject x3 =
  Bind_new.Bret x3

(** val dpi1__o__blist_from_list :
    ('a2 List.list, 'a3) Types.dPair -> ('a1, 'a2 List.list)
    Bind_new.bind_new **)
let dpi1__o__blist_from_list x3 =
  let l = x3.Types.dpi1 in Bind_new.Bret l

(** val eject__o__blist_from_list :
    'a2 List.list Types.sig0 -> ('a1, 'a2 List.list) Bind_new.bind_new **)
let eject__o__blist_from_list x3 =
  let l = Types.pi1 x3 in Bind_new.Bret l

(** val bappend :
    ('a1, 'a2) bind_list -> ('a1, 'a2) bind_list -> ('a1, 'a2) bind_list **)
let bappend x =
  Obj.magic
    (Monad.m_bin_op (Monad.max_def Bind_new.bindNew) List.append
      (Obj.magic x))

open Option

open Extranat

open Div_and_mod

open Util

open Vector

(** val bcons : 'a2 -> ('a1, 'a2) bind_list -> ('a1, 'a2) bind_list **)
let bcons e =
  Obj.magic
    (Monad.m_map (Monad.max_def Bind_new.bindNew) (fun x -> List.Cons (e,
      x)))

open Lists