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

val eject__o__blist_from_list__o__inject :
  'a2 List.list Types.sig0 -> ('a1, 'a2 List.list) Bind_new.bind_new
  Types.sig0

val blist_from_list__o__inject :
  'a2 List.list -> ('a1, 'a2 List.list) Bind_new.bind_new Types.sig0

val dpi1__o__blist_from_list :
  ('a2 List.list, 'a3) Types.dPair -> ('a1, 'a2 List.list) Bind_new.bind_new

val eject__o__blist_from_list :
  'a2 List.list Types.sig0 -> ('a1, 'a2 List.list) Bind_new.bind_new

val bappend :
  ('a1, 'a2) bind_list -> ('a1, 'a2) bind_list -> ('a1, 'a2) bind_list

open Option

open Extranat

open Div_and_mod

open Util

open Vector

val bcons : 'a2 -> ('a1, 'a2) bind_list -> ('a1, 'a2) bind_list

open Lists