open Preamble

open Hints_declaration

open Core_notation

open Pts

open Logic

open Types

open Bool

open Relations

open Nat

open List

open Positive

open PreIdentifiers

open Jmeq

open Russell

open Setoids

open Monad

open Option

open ErrorMessages

type errcode =
| MSG of ErrorMessages.errorMessage
| CTX of PreIdentifiers.identifierTag * PreIdentifiers.identifier

val errcode_rect_Type4 :
  (ErrorMessages.errorMessage -> 'a1) -> (PreIdentifiers.identifierTag ->
  PreIdentifiers.identifier -> 'a1) -> errcode -> 'a1

val errcode_rect_Type5 :
  (ErrorMessages.errorMessage -> 'a1) -> (PreIdentifiers.identifierTag ->
  PreIdentifiers.identifier -> 'a1) -> errcode -> 'a1

val errcode_rect_Type3 :
  (ErrorMessages.errorMessage -> 'a1) -> (PreIdentifiers.identifierTag ->
  PreIdentifiers.identifier -> 'a1) -> errcode -> 'a1

val errcode_rect_Type2 :
  (ErrorMessages.errorMessage -> 'a1) -> (PreIdentifiers.identifierTag ->
  PreIdentifiers.identifier -> 'a1) -> errcode -> 'a1

val errcode_rect_Type1 :
  (ErrorMessages.errorMessage -> 'a1) -> (PreIdentifiers.identifierTag ->
  PreIdentifiers.identifier -> 'a1) -> errcode -> 'a1

val errcode_rect_Type0 :
  (ErrorMessages.errorMessage -> 'a1) -> (PreIdentifiers.identifierTag ->
  PreIdentifiers.identifier -> 'a1) -> errcode -> 'a1

val errcode_inv_rect_Type4 :
  errcode -> (ErrorMessages.errorMessage -> __ -> 'a1) ->
  (PreIdentifiers.identifierTag -> PreIdentifiers.identifier -> __ -> 'a1) ->
  'a1

val errcode_inv_rect_Type3 :
  errcode -> (ErrorMessages.errorMessage -> __ -> 'a1) ->
  (PreIdentifiers.identifierTag -> PreIdentifiers.identifier -> __ -> 'a1) ->
  'a1

val errcode_inv_rect_Type2 :
  errcode -> (ErrorMessages.errorMessage -> __ -> 'a1) ->
  (PreIdentifiers.identifierTag -> PreIdentifiers.identifier -> __ -> 'a1) ->
  'a1

val errcode_inv_rect_Type1 :
  errcode -> (ErrorMessages.errorMessage -> __ -> 'a1) ->
  (PreIdentifiers.identifierTag -> PreIdentifiers.identifier -> __ -> 'a1) ->
  'a1

val errcode_inv_rect_Type0 :
  errcode -> (ErrorMessages.errorMessage -> __ -> 'a1) ->
  (PreIdentifiers.identifierTag -> PreIdentifiers.identifier -> __ -> 'a1) ->
  'a1

val errcode_discr : errcode -> errcode -> __

val errcode_jmdiscr : errcode -> errcode -> __

type errmsg = errcode List.list

val msg : ErrorMessages.errorMessage -> errmsg

type 'a res =
| OK of 'a
| Error of errmsg

val res_rect_Type4 : ('a1 -> 'a2) -> (errmsg -> 'a2) -> 'a1 res -> 'a2

val res_rect_Type5 : ('a1 -> 'a2) -> (errmsg -> 'a2) -> 'a1 res -> 'a2

val res_rect_Type3 : ('a1 -> 'a2) -> (errmsg -> 'a2) -> 'a1 res -> 'a2

val res_rect_Type2 : ('a1 -> 'a2) -> (errmsg -> 'a2) -> 'a1 res -> 'a2

val res_rect_Type1 : ('a1 -> 'a2) -> (errmsg -> 'a2) -> 'a1 res -> 'a2

val res_rect_Type0 : ('a1 -> 'a2) -> (errmsg -> 'a2) -> 'a1 res -> 'a2

val res_inv_rect_Type4 :
  'a1 res -> ('a1 -> __ -> 'a2) -> (errmsg -> __ -> 'a2) -> 'a2

val res_inv_rect_Type3 :
  'a1 res -> ('a1 -> __ -> 'a2) -> (errmsg -> __ -> 'a2) -> 'a2

val res_inv_rect_Type2 :
  'a1 res -> ('a1 -> __ -> 'a2) -> (errmsg -> __ -> 'a2) -> 'a2

val res_inv_rect_Type1 :
  'a1 res -> ('a1 -> __ -> 'a2) -> (errmsg -> __ -> 'a2) -> 'a2

val res_inv_rect_Type0 :
  'a1 res -> ('a1 -> __ -> 'a2) -> (errmsg -> __ -> 'a2) -> 'a2

val res_discr : 'a1 res -> 'a1 res -> __

val res_jmdiscr : 'a1 res -> 'a1 res -> __

val res0 : Monad.monadProps

val mfold_left_i_aux :
  (Nat.nat -> 'a1 -> 'a2 -> 'a1 res) -> 'a1 res -> Nat.nat -> 'a2 List.list
  -> __

val mfold_left_i :
  (Nat.nat -> 'a1 -> 'a2 -> 'a1 res) -> 'a1 res -> 'a2 List.list -> __

val mfold_left2 :
  ('a1 -> 'a2 -> 'a3 -> 'a1 res) -> 'a1 res -> 'a2 List.list -> 'a3 List.list
  -> 'a1 res

val opt_to_res : errmsg -> 'a1 Types.option -> 'a1 res

val jmeq_to_eq__o__opt_eq_from_res__o__inject :
  errmsg -> 'a1 Types.option -> 'a1 -> __ Types.sig0

val dpi1__o__opt_eq_from_res__o__inject :
  errmsg -> 'a1 Types.option -> 'a1 -> (__, 'a2) Types.dPair -> __ Types.sig0

val eject__o__opt_eq_from_res__o__inject :
  errmsg -> 'a1 Types.option -> 'a1 -> __ Types.sig0 -> __ Types.sig0

val opt_eq_from_res__o__inject :
  errmsg -> 'a1 Types.option -> 'a1 -> __ Types.sig0

val bind_eq : 'a1 res -> ('a1 -> __ -> 'a2 res) -> 'a2 res

val bind2_eq :
  ('a1, 'a2) Types.prod res -> ('a1 -> 'a2 -> __ -> 'a3 res) -> 'a3 res

val res_to_opt : 'a1 res -> 'a1 Types.option

val bind : __ -> ('a1 -> __) -> __

val bind2 : __ -> ('a1 -> 'a2 -> __) -> __

val bind3 : __ -> ('a1 -> 'a2 -> 'a3 -> __) -> __

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

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