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

val setoid_rect_Type5 : (__ -> __ -> __ -> __ -> __ -> 'a1) -> setoid -> 'a1

val setoid_rect_Type3 : (__ -> __ -> __ -> __ -> __ -> 'a1) -> setoid -> 'a1

val setoid_rect_Type2 : (__ -> __ -> __ -> __ -> __ -> 'a1) -> setoid -> 'a1

val setoid_rect_Type1 : (__ -> __ -> __ -> __ -> __ -> 'a1) -> setoid -> 'a1

val setoid_rect_Type0 : (__ -> __ -> __ -> __ -> __ -> 'a1) -> setoid -> 'a1

type std_supp 

val setoid_inv_rect_Type4 :
  setoid -> (__ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1

val setoid_inv_rect_Type3 :
  setoid -> (__ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1

val setoid_inv_rect_Type2 :
  setoid -> (__ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1

val setoid_inv_rect_Type1 :
  setoid -> (__ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1

val setoid_inv_rect_Type0 :
  setoid -> (__ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1

val as_std : setoid

val std_prod : setoid -> setoid -> setoid

val std_union : setoid -> setoid -> setoid