open Preamble

open Hints_declaration

open Core_notation

open Pts

open Logic

open Types

open Bool

open Relations

open Nat

open Positive

open Setoids

open Monad

open Option

open Div_and_mod

open Jmeq

open Russell

open Util

open List

open Lists

open Extralib

open ErrorMessages

open PreIdentifiers

open Errors

type universe =
  Positive.pos
  (* singleton inductive, whose constructor was mk_universe *)

val universe_rect_Type4 :
  PreIdentifiers.identifierTag -> (Positive.pos -> 'a1) -> universe -> 'a1

val universe_rect_Type5 :
  PreIdentifiers.identifierTag -> (Positive.pos -> 'a1) -> universe -> 'a1

val universe_rect_Type3 :
  PreIdentifiers.identifierTag -> (Positive.pos -> 'a1) -> universe -> 'a1

val universe_rect_Type2 :
  PreIdentifiers.identifierTag -> (Positive.pos -> 'a1) -> universe -> 'a1

val universe_rect_Type1 :
  PreIdentifiers.identifierTag -> (Positive.pos -> 'a1) -> universe -> 'a1

val universe_rect_Type0 :
  PreIdentifiers.identifierTag -> (Positive.pos -> 'a1) -> universe -> 'a1

val next_identifier :
  PreIdentifiers.identifierTag -> universe -> Positive.pos

val universe_inv_rect_Type4 :
  PreIdentifiers.identifierTag -> universe -> (Positive.pos -> __ -> 'a1) ->
  'a1

val universe_inv_rect_Type3 :
  PreIdentifiers.identifierTag -> universe -> (Positive.pos -> __ -> 'a1) ->
  'a1

val universe_inv_rect_Type2 :
  PreIdentifiers.identifierTag -> universe -> (Positive.pos -> __ -> 'a1) ->
  'a1

val universe_inv_rect_Type1 :
  PreIdentifiers.identifierTag -> universe -> (Positive.pos -> __ -> 'a1) ->
  'a1

val universe_inv_rect_Type0 :
  PreIdentifiers.identifierTag -> universe -> (Positive.pos -> __ -> 'a1) ->
  'a1

val universe_discr :
  PreIdentifiers.identifierTag -> universe -> universe -> __

val universe_jmdiscr :
  PreIdentifiers.identifierTag -> universe -> universe -> __

val new_universe : PreIdentifiers.identifierTag -> universe

val fresh :
  PreIdentifiers.identifierTag -> universe -> (PreIdentifiers.identifier,
  universe) Types.prod

val eq_identifier :
  PreIdentifiers.identifierTag -> PreIdentifiers.identifier ->
  PreIdentifiers.identifier -> Bool.bool

val eq_identifier_elim :
  PreIdentifiers.identifierTag -> PreIdentifiers.identifier ->
  PreIdentifiers.identifier -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

open Deqsets

val deq_identifier : PreIdentifiers.identifierTag -> Deqsets.deqSet

val word_of_identifier :
  PreIdentifiers.identifierTag -> PreIdentifiers.identifier -> Positive.pos

val identifier_eq :
  PreIdentifiers.identifierTag -> PreIdentifiers.identifier ->
  PreIdentifiers.identifier -> (__, __) Types.sum

val identifier_of_nat :
  PreIdentifiers.identifierTag -> Nat.nat -> PreIdentifiers.identifier

val check_member_env :
  PreIdentifiers.identifierTag -> PreIdentifiers.identifier ->
  (PreIdentifiers.identifier, 'a1) Types.prod List.list -> __ Errors.res

val check_distinct_env :
  PreIdentifiers.identifierTag -> (PreIdentifiers.identifier, 'a1) Types.prod
  List.list -> __ Errors.res

open PositiveMap

type 'a identifier_map =
  'a PositiveMap.positive_map
  (* singleton inductive, whose constructor was an_id_map *)

val identifier_map_rect_Type4 :
  PreIdentifiers.identifierTag -> ('a1 PositiveMap.positive_map -> 'a2) ->
  'a1 identifier_map -> 'a2

val identifier_map_rect_Type5 :
  PreIdentifiers.identifierTag -> ('a1 PositiveMap.positive_map -> 'a2) ->
  'a1 identifier_map -> 'a2

val identifier_map_rect_Type3 :
  PreIdentifiers.identifierTag -> ('a1 PositiveMap.positive_map -> 'a2) ->
  'a1 identifier_map -> 'a2

val identifier_map_rect_Type2 :
  PreIdentifiers.identifierTag -> ('a1 PositiveMap.positive_map -> 'a2) ->
  'a1 identifier_map -> 'a2

val identifier_map_rect_Type1 :
  PreIdentifiers.identifierTag -> ('a1 PositiveMap.positive_map -> 'a2) ->
  'a1 identifier_map -> 'a2

val identifier_map_rect_Type0 :
  PreIdentifiers.identifierTag -> ('a1 PositiveMap.positive_map -> 'a2) ->
  'a1 identifier_map -> 'a2

val identifier_map_inv_rect_Type4 :
  PreIdentifiers.identifierTag -> 'a1 identifier_map -> ('a1
  PositiveMap.positive_map -> __ -> 'a2) -> 'a2

val identifier_map_inv_rect_Type3 :
  PreIdentifiers.identifierTag -> 'a1 identifier_map -> ('a1
  PositiveMap.positive_map -> __ -> 'a2) -> 'a2

val identifier_map_inv_rect_Type2 :
  PreIdentifiers.identifierTag -> 'a1 identifier_map -> ('a1
  PositiveMap.positive_map -> __ -> 'a2) -> 'a2

val identifier_map_inv_rect_Type1 :
  PreIdentifiers.identifierTag -> 'a1 identifier_map -> ('a1
  PositiveMap.positive_map -> __ -> 'a2) -> 'a2

val identifier_map_inv_rect_Type0 :
  PreIdentifiers.identifierTag -> 'a1 identifier_map -> ('a1
  PositiveMap.positive_map -> __ -> 'a2) -> 'a2

val identifier_map_discr :
  PreIdentifiers.identifierTag -> 'a1 identifier_map -> 'a1 identifier_map ->
  __

val identifier_map_jmdiscr :
  PreIdentifiers.identifierTag -> 'a1 identifier_map -> 'a1 identifier_map ->
  __

val empty_map : PreIdentifiers.identifierTag -> 'a1 identifier_map

val lookup :
  PreIdentifiers.identifierTag -> 'a1 identifier_map ->
  PreIdentifiers.identifier -> 'a1 Types.option

val lookup_def :
  PreIdentifiers.identifierTag -> 'a1 identifier_map ->
  PreIdentifiers.identifier -> 'a1 -> 'a1

val member :
  PreIdentifiers.identifierTag -> 'a1 identifier_map ->
  PreIdentifiers.identifier -> Bool.bool

val lookup_safe :
  PreIdentifiers.identifierTag -> 'a1 identifier_map ->
  PreIdentifiers.identifier -> 'a1

val add :
  PreIdentifiers.identifierTag -> 'a1 identifier_map ->
  PreIdentifiers.identifier -> 'a1 -> 'a1 identifier_map

val elements :
  PreIdentifiers.identifierTag -> 'a1 identifier_map ->
  (PreIdentifiers.identifier, 'a1) Types.prod List.list

val idmap_all :
  PreIdentifiers.identifierTag -> 'a1 identifier_map ->
  (PreIdentifiers.identifier -> 'a1 -> __ -> Bool.bool) -> Bool.bool

val update :
  PreIdentifiers.identifierTag -> 'a1 identifier_map ->
  PreIdentifiers.identifier -> 'a1 -> 'a1 identifier_map Errors.res

val remove :
  PreIdentifiers.identifierTag -> 'a1 identifier_map ->
  PreIdentifiers.identifier -> 'a1 identifier_map

val foldi :
  PreIdentifiers.identifierTag -> (PreIdentifiers.identifier -> 'a1 -> 'a2 ->
  'a2) -> 'a1 identifier_map -> 'a2 -> 'a2

val fold_inf :
  PreIdentifiers.identifierTag -> 'a1 identifier_map ->
  (PreIdentifiers.identifier -> 'a1 -> __ -> 'a2 -> 'a2) -> 'a2 -> 'a2

val find :
  PreIdentifiers.identifierTag -> 'a1 identifier_map ->
  (PreIdentifiers.identifier -> 'a1 -> Bool.bool) ->
  (PreIdentifiers.identifier, 'a1) Types.prod Types.option

val lookup_present :
  PreIdentifiers.identifierTag -> 'a1 identifier_map ->
  PreIdentifiers.identifier -> 'a1

val update_present :
  PreIdentifiers.identifierTag -> 'a1 identifier_map ->
  PreIdentifiers.identifier -> 'a1 -> 'a1 identifier_map

type identifier_set = Types.unit0 identifier_map

val empty_set : PreIdentifiers.identifierTag -> identifier_set

val add_set :
  PreIdentifiers.identifierTag -> identifier_set -> PreIdentifiers.identifier
  -> identifier_set

val singleton_set :
  PreIdentifiers.identifierTag -> PreIdentifiers.identifier -> identifier_set

val union_set :
  PreIdentifiers.identifierTag -> 'a1 identifier_map -> 'a2 identifier_map ->
  identifier_set

val minus_set :
  PreIdentifiers.identifierTag -> 'a1 identifier_map -> 'a2 identifier_map ->
  'a1 identifier_map

val identifierSet : PreIdentifiers.identifierTag -> Setoids.setoid

val id_map_size :
  PreIdentifiers.identifierTag -> 'a1 identifier_map -> Nat.nat

open Proper

val set_from_list :
  PreIdentifiers.identifierTag -> PreIdentifiers.identifier List.list ->
  Types.unit0 identifier_map

val dpi1__o__id_set_from_list__o__inject :
  PreIdentifiers.identifierTag -> (PreIdentifiers.identifier List.list, 'a1)
  Types.dPair -> Types.unit0 identifier_map Types.sig0

val eject__o__id_set_from_list__o__inject :
  PreIdentifiers.identifierTag -> PreIdentifiers.identifier List.list
  Types.sig0 -> Types.unit0 identifier_map Types.sig0

val id_set_from_list__o__inject :
  PreIdentifiers.identifierTag -> PreIdentifiers.identifier List.list ->
  Types.unit0 identifier_map Types.sig0

val dpi1__o__id_set_from_list :
  PreIdentifiers.identifierTag -> (PreIdentifiers.identifier List.list, 'a1)
  Types.dPair -> Types.unit0 identifier_map

val eject__o__id_set_from_list :
  PreIdentifiers.identifierTag -> PreIdentifiers.identifier List.list
  Types.sig0 -> Types.unit0 identifier_map

val choose :
  PreIdentifiers.identifierTag -> 'a1 identifier_map ->
  ((PreIdentifiers.identifier, 'a1) Types.prod, 'a1 identifier_map)
  Types.prod Types.option

val try_remove :
  PreIdentifiers.identifierTag -> 'a1 identifier_map ->
  PreIdentifiers.identifier -> ('a1, 'a1 identifier_map) Types.prod
  Types.option

val id_set_of_map :
  PreIdentifiers.identifierTag -> 'a1 identifier_map -> identifier_set

val set_of_list :
  PreIdentifiers.identifierTag -> PreIdentifiers.identifier List.list ->
  identifier_set

val domain_of_map :
  PreIdentifiers.identifierTag -> 'a1 identifier_map -> identifier_set