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 **)
let rec deqSet_rect_Type4 h_mk_DeqSet x_3369 =
  let eqb = x_3369 in h_mk_DeqSet __ eqb __

(** val deqSet_rect_Type5 :
    (__ -> (__ -> __ -> Bool.bool) -> __ -> 'a1) -> deqSet -> 'a1 **)
let rec deqSet_rect_Type5 h_mk_DeqSet x_3371 =
  let eqb = x_3371 in h_mk_DeqSet __ eqb __

(** val deqSet_rect_Type3 :
    (__ -> (__ -> __ -> Bool.bool) -> __ -> 'a1) -> deqSet -> 'a1 **)
let rec deqSet_rect_Type3 h_mk_DeqSet x_3373 =
  let eqb = x_3373 in h_mk_DeqSet __ eqb __

(** val deqSet_rect_Type2 :
    (__ -> (__ -> __ -> Bool.bool) -> __ -> 'a1) -> deqSet -> 'a1 **)
let rec deqSet_rect_Type2 h_mk_DeqSet x_3375 =
  let eqb = x_3375 in h_mk_DeqSet __ eqb __

(** val deqSet_rect_Type1 :
    (__ -> (__ -> __ -> Bool.bool) -> __ -> 'a1) -> deqSet -> 'a1 **)
let rec deqSet_rect_Type1 h_mk_DeqSet x_3377 =
  let eqb = x_3377 in h_mk_DeqSet __ eqb __

(** val deqSet_rect_Type0 :
    (__ -> (__ -> __ -> Bool.bool) -> __ -> 'a1) -> deqSet -> 'a1 **)
let rec deqSet_rect_Type0 h_mk_DeqSet x_3379 =
  let eqb = x_3379 in h_mk_DeqSet __ eqb __

type carr = __

(** val eqb : deqSet -> __ -> __ -> Bool.bool **)
let rec eqb xxx =
  let yyy = xxx in yyy

(** val deqSet_inv_rect_Type4 :
    deqSet -> (__ -> (__ -> __ -> Bool.bool) -> __ -> __ -> 'a1) -> 'a1 **)
let deqSet_inv_rect_Type4 hterm h1 =
  let hcut = deqSet_rect_Type4 h1 hterm in hcut __

(** val deqSet_inv_rect_Type3 :
    deqSet -> (__ -> (__ -> __ -> Bool.bool) -> __ -> __ -> 'a1) -> 'a1 **)
let deqSet_inv_rect_Type3 hterm h1 =
  let hcut = deqSet_rect_Type3 h1 hterm in hcut __

(** val deqSet_inv_rect_Type2 :
    deqSet -> (__ -> (__ -> __ -> Bool.bool) -> __ -> __ -> 'a1) -> 'a1 **)
let deqSet_inv_rect_Type2 hterm h1 =
  let hcut = deqSet_rect_Type2 h1 hterm in hcut __

(** val deqSet_inv_rect_Type1 :
    deqSet -> (__ -> (__ -> __ -> Bool.bool) -> __ -> __ -> 'a1) -> 'a1 **)
let deqSet_inv_rect_Type1 hterm h1 =
  let hcut = deqSet_rect_Type1 h1 hterm in hcut __

(** val deqSet_inv_rect_Type0 :
    deqSet -> (__ -> (__ -> __ -> Bool.bool) -> __ -> __ -> 'a1) -> 'a1 **)
let deqSet_inv_rect_Type0 hterm h1 =
  let hcut = deqSet_rect_Type0 h1 hterm in hcut __

(** val beqb : Bool.bool -> Bool.bool -> Bool.bool **)
let beqb b1 b2 =
  match b1 with
  | Bool.True -> b2
  | Bool.False -> Bool.notb b2

(** val deqBool : deqSet **)
let deqBool =
  Obj.magic beqb

(** val eq_option :
    deqSet -> __ Types.option -> __ Types.option -> Bool.bool **)
let eq_option a a1 a2 =
  match a1 with
  | Types.None ->
    (match a2 with
     | Types.None -> Bool.True
     | Types.Some x -> Bool.False)
  | Types.Some a1' ->
    (match a2 with
     | Types.None -> Bool.False
     | Types.Some a2' -> eqb a a1' a2')

(** val deqOption : deqSet -> deqSet **)
let deqOption a =
  Obj.magic (eq_option a)

(** val eq_pairs :
    deqSet -> deqSet -> (__, __) Types.prod -> (__, __) Types.prod ->
    Bool.bool **)
let eq_pairs a b p1 p2 =
  Bool.andb (eqb a p1.Types.fst p2.Types.fst)
    (eqb b p1.Types.snd p2.Types.snd)

(** val deqProd : deqSet -> deqSet -> deqSet **)
let deqProd a b =
  Obj.magic (eq_pairs a b)

(** val eq_sum :
    deqSet -> deqSet -> (__, __) Types.sum -> (__, __) Types.sum -> Bool.bool **)
let eq_sum a b p1 p2 =
  match p1 with
  | Types.Inl a1 ->
    (match p2 with
     | Types.Inl a2 -> eqb a a1 a2
     | Types.Inr b2 -> Bool.False)
  | Types.Inr b1 ->
    (match p2 with
     | Types.Inl a2 -> Bool.False
     | Types.Inr b2 -> eqb b b1 b2)

(** val deqSum : deqSet -> deqSet -> deqSet **)
let deqSum a b =
  Obj.magic (eq_sum a b)

(** val eq_sigma : deqSet -> __ Types.sig0 -> __ Types.sig0 -> Bool.bool **)
let eq_sigma a p1 p2 =
  let a1 = p1 in let a2 = p2 in eqb a a1 a2

(** val deqSig : deqSet -> deqSet **)
let deqSig a =
  Obj.magic (eq_sigma a)