open Preamble

open Bool

open Relations

open Nat

open Hints_declaration

open Core_notation

open Pts

open Logic

open Types

open List

open Div_and_mod

open Jmeq

open Russell

open Util

val all : ('a1 -> Bool.bool) -> 'a1 List.list -> Bool.bool

val map_All : ('a1 -> __ -> 'a2) -> 'a1 List.list -> 'a2 List.list

open Setoids

open Monad

open Option

val append : 'a1 List.list List.aop

val list : Monad.monadProps

val count : ('a1 -> Bool.bool) -> 'a1 List.list -> Nat.nat

val position_of_safe : ('a1 -> Bool.bool) -> 'a1 List.list -> Nat.nat

val index_of : ('a1 -> Bool.bool) -> 'a1 List.list -> Nat.nat

val ordered_insert :
  ('a1 -> 'a1 -> Bool.bool) -> 'a1 -> 'a1 List.list -> 'a1 List.list

val insert_sort : ('a1 -> 'a1 -> Bool.bool) -> 'a1 List.list -> 'a1 List.list

val range_strong_internal :
  Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat Types.sig0 List.list

val range_strong : Nat.nat -> Nat.nat Types.sig0 List.list