open Preamble

open Hints_declaration

open Core_notation

open Pts

open Logic

open Types

open Bool

open Relations

open Nat

open List

open Div_and_mod

open Jmeq

open Russell

open Util

val eq_rect_Type0_r : 'a1 -> 'a2 -> 'a1 -> 'a2

val eq_rect_r2 : 'a1 -> 'a1 -> 'a2 -> 'a2

val eq_rect_Type2_r : 'a1 -> 'a2 -> 'a1 -> 'a2

val dec_bounded_forall :
  (Nat.nat -> (__, __) Types.sum) -> Nat.nat -> (__, __) Types.sum

val dec_bounded_exists :
  (Nat.nat -> (__, __) Types.sum) -> Nat.nat -> (__, __) Types.sum

val dec_true : (__, __) Types.sum -> (__ -> 'a1) -> 'a1

val dec_false : (__, __) Types.sum -> (__ -> 'a1) -> 'a1