open Preamble

open Hints_declaration

open Core_notation

open Pts

open Logic

open Types

open Relations

open Bool

type deqSet =
  __ -> __ -> Bool.bool
  (* singleton inductive, whose constructor was mk_DeqSet *)

val deqSet_rect_Type4 :
  (__ -> (__ -> __ -> Bool.bool) -> __ -> 'a1) -> deqSet -> 'a1

val deqSet_rect_Type5 :
  (__ -> (__ -> __ -> Bool.bool) -> __ -> 'a1) -> deqSet -> 'a1

val deqSet_rect_Type3 :
  (__ -> (__ -> __ -> Bool.bool) -> __ -> 'a1) -> deqSet -> 'a1

val deqSet_rect_Type2 :
  (__ -> (__ -> __ -> Bool.bool) -> __ -> 'a1) -> deqSet -> 'a1

val deqSet_rect_Type1 :
  (__ -> (__ -> __ -> Bool.bool) -> __ -> 'a1) -> deqSet -> 'a1

val deqSet_rect_Type0 :
  (__ -> (__ -> __ -> Bool.bool) -> __ -> 'a1) -> deqSet -> 'a1

type carr 

val eqb : deqSet -> __ -> __ -> Bool.bool

val deqSet_inv_rect_Type4 :
  deqSet -> (__ -> (__ -> __ -> Bool.bool) -> __ -> __ -> 'a1) -> 'a1

val deqSet_inv_rect_Type3 :
  deqSet -> (__ -> (__ -> __ -> Bool.bool) -> __ -> __ -> 'a1) -> 'a1

val deqSet_inv_rect_Type2 :
  deqSet -> (__ -> (__ -> __ -> Bool.bool) -> __ -> __ -> 'a1) -> 'a1

val deqSet_inv_rect_Type1 :
  deqSet -> (__ -> (__ -> __ -> Bool.bool) -> __ -> __ -> 'a1) -> 'a1

val deqSet_inv_rect_Type0 :
  deqSet -> (__ -> (__ -> __ -> Bool.bool) -> __ -> __ -> 'a1) -> 'a1

val beqb : Bool.bool -> Bool.bool -> Bool.bool

val deqBool : deqSet

val eq_option : deqSet -> __ Types.option -> __ Types.option -> Bool.bool

val deqOption : deqSet -> deqSet

val eq_pairs :
  deqSet -> deqSet -> (__, __) Types.prod -> (__, __) Types.prod -> Bool.bool

val deqProd : deqSet -> deqSet -> deqSet

val eq_sum :
  deqSet -> deqSet -> (__, __) Types.sum -> (__, __) Types.sum -> Bool.bool

val deqSum : deqSet -> deqSet -> deqSet

val eq_sigma : deqSet -> __ Types.sig0 -> __ Types.sig0 -> Bool.bool

val deqSig : deqSet -> deqSet