open Preamble

open Core_notation

open Pts

open Hints_declaration

open Logic

open Types

open Relations

type setoid =
| Mk_Setoid

(** val setoid_rect_Type4 :
    (__ -> __ -> __ -> __ -> __ -> 'a1) -> setoid -> 'a1 **)
let rec setoid_rect_Type4 h_mk_Setoid = function
| Mk_Setoid -> h_mk_Setoid __ __ __ __ __

(** val setoid_rect_Type5 :
    (__ -> __ -> __ -> __ -> __ -> 'a1) -> setoid -> 'a1 **)
let rec setoid_rect_Type5 h_mk_Setoid = function
| Mk_Setoid -> h_mk_Setoid __ __ __ __ __

(** val setoid_rect_Type3 :
    (__ -> __ -> __ -> __ -> __ -> 'a1) -> setoid -> 'a1 **)
let rec setoid_rect_Type3 h_mk_Setoid = function
| Mk_Setoid -> h_mk_Setoid __ __ __ __ __

(** val setoid_rect_Type2 :
    (__ -> __ -> __ -> __ -> __ -> 'a1) -> setoid -> 'a1 **)
let rec setoid_rect_Type2 h_mk_Setoid = function
| Mk_Setoid -> h_mk_Setoid __ __ __ __ __

(** val setoid_rect_Type1 :
    (__ -> __ -> __ -> __ -> __ -> 'a1) -> setoid -> 'a1 **)
let rec setoid_rect_Type1 h_mk_Setoid = function
| Mk_Setoid -> h_mk_Setoid __ __ __ __ __

(** val setoid_rect_Type0 :
    (__ -> __ -> __ -> __ -> __ -> 'a1) -> setoid -> 'a1 **)
let rec setoid_rect_Type0 h_mk_Setoid = function
| Mk_Setoid -> h_mk_Setoid __ __ __ __ __

type std_supp = __

(** val setoid_inv_rect_Type4 :
    setoid -> (__ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
let setoid_inv_rect_Type4 hterm h1 =
  let hcut = setoid_rect_Type4 h1 hterm in hcut __

(** val setoid_inv_rect_Type3 :
    setoid -> (__ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
let setoid_inv_rect_Type3 hterm h1 =
  let hcut = setoid_rect_Type3 h1 hterm in hcut __

(** val setoid_inv_rect_Type2 :
    setoid -> (__ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
let setoid_inv_rect_Type2 hterm h1 =
  let hcut = setoid_rect_Type2 h1 hterm in hcut __

(** val setoid_inv_rect_Type1 :
    setoid -> (__ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
let setoid_inv_rect_Type1 hterm h1 =
  let hcut = setoid_rect_Type1 h1 hterm in hcut __

(** val setoid_inv_rect_Type0 :
    setoid -> (__ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
let setoid_inv_rect_Type0 hterm h1 =
  let hcut = setoid_rect_Type0 h1 hterm in hcut __

(** val as_std : setoid **)
let as_std =
  Mk_Setoid

(** val std_prod : setoid -> setoid -> setoid **)
let std_prod x y =
  Mk_Setoid

(** val std_union : setoid -> setoid -> setoid **)
let std_union x y =
  Mk_Setoid