18 (** val setoid_rect_Type4 :
19 (__ -> __ -> __ -> __ -> __ -> 'a1) -> setoid -> 'a1 **)
20 let rec setoid_rect_Type4 h_mk_Setoid = function
21 | Mk_Setoid -> h_mk_Setoid __ __ __ __ __
23 (** val setoid_rect_Type5 :
24 (__ -> __ -> __ -> __ -> __ -> 'a1) -> setoid -> 'a1 **)
25 let rec setoid_rect_Type5 h_mk_Setoid = function
26 | Mk_Setoid -> h_mk_Setoid __ __ __ __ __
28 (** val setoid_rect_Type3 :
29 (__ -> __ -> __ -> __ -> __ -> 'a1) -> setoid -> 'a1 **)
30 let rec setoid_rect_Type3 h_mk_Setoid = function
31 | Mk_Setoid -> h_mk_Setoid __ __ __ __ __
33 (** val setoid_rect_Type2 :
34 (__ -> __ -> __ -> __ -> __ -> 'a1) -> setoid -> 'a1 **)
35 let rec setoid_rect_Type2 h_mk_Setoid = function
36 | Mk_Setoid -> h_mk_Setoid __ __ __ __ __
38 (** val setoid_rect_Type1 :
39 (__ -> __ -> __ -> __ -> __ -> 'a1) -> setoid -> 'a1 **)
40 let rec setoid_rect_Type1 h_mk_Setoid = function
41 | Mk_Setoid -> h_mk_Setoid __ __ __ __ __
43 (** val setoid_rect_Type0 :
44 (__ -> __ -> __ -> __ -> __ -> 'a1) -> setoid -> 'a1 **)
45 let rec setoid_rect_Type0 h_mk_Setoid = function
46 | Mk_Setoid -> h_mk_Setoid __ __ __ __ __
50 (** val setoid_inv_rect_Type4 :
51 setoid -> (__ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
52 let setoid_inv_rect_Type4 hterm h1 =
53 let hcut = setoid_rect_Type4 h1 hterm in hcut __
55 (** val setoid_inv_rect_Type3 :
56 setoid -> (__ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
57 let setoid_inv_rect_Type3 hterm h1 =
58 let hcut = setoid_rect_Type3 h1 hterm in hcut __
60 (** val setoid_inv_rect_Type2 :
61 setoid -> (__ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
62 let setoid_inv_rect_Type2 hterm h1 =
63 let hcut = setoid_rect_Type2 h1 hterm in hcut __
65 (** val setoid_inv_rect_Type1 :
66 setoid -> (__ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
67 let setoid_inv_rect_Type1 hterm h1 =
68 let hcut = setoid_rect_Type1 h1 hterm in hcut __
70 (** val setoid_inv_rect_Type0 :
71 setoid -> (__ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
72 let setoid_inv_rect_Type0 hterm h1 =
73 let hcut = setoid_rect_Type0 h1 hterm in hcut __
75 (** val as_std : setoid **)
79 (** val std_prod : setoid -> setoid -> setoid **)
83 (** val std_union : setoid -> setoid -> setoid **)