9 (** val eq_rect_Type4 : 'a1 -> 'a2 -> 'a1 -> 'a2 **)
10 let rec eq_rect_Type4 x h_refl x_4 =
13 (** val eq_rect_Type5 : 'a1 -> 'a2 -> 'a1 -> 'a2 **)
14 let rec eq_rect_Type5 x h_refl x_7 =
17 (** val eq_rect_Type3 : 'a1 -> 'a2 -> 'a1 -> 'a2 **)
18 let rec eq_rect_Type3 x h_refl x_10 =
21 (** val eq_rect_Type2 : 'a1 -> 'a2 -> 'a1 -> 'a2 **)
22 let rec eq_rect_Type2 x h_refl x_13 =
25 (** val eq_rect_Type1 : 'a1 -> 'a2 -> 'a1 -> 'a2 **)
26 let rec eq_rect_Type1 x h_refl x_16 =
29 (** val eq_rect_Type0 : 'a1 -> 'a2 -> 'a1 -> 'a2 **)
30 let rec eq_rect_Type0 x h_refl x_19 =
33 (** val eq_rect_r : 'a1 -> 'a1 -> 'a2 -> 'a2 **)
34 let eq_rect_r a x x0 =
35 (fun _ auto -> auto) __ x0
37 (** val eq_rect_Type0_r : 'a1 -> 'a2 -> 'a1 -> 'a2 **)
38 let eq_rect_Type0_r a h x =
39 (fun _ auto -> auto) __ h
41 (** val eq_rect_Type1_r : 'a1 -> 'a2 -> 'a1 -> 'a2 **)
42 let eq_rect_Type1_r a h x =
43 (fun _ auto -> auto) __ h
45 (** val eq_rect_Type2_r : 'a1 -> 'a2 -> 'a1 -> 'a2 **)
46 let eq_rect_Type2_r a h x =
47 (fun _ auto -> auto) __ h
49 (** val eq_rect_Type3_r : 'a1 -> 'a2 -> 'a1 -> 'a2 **)
50 let eq_rect_Type3_r a h x =
51 (fun _ auto -> auto) __ h
53 (** val rewrite_l : 'a1 -> 'a2 -> 'a1 -> 'a2 **)
54 let rewrite_l x hx y =
57 (** val rewrite_r : 'a1 -> 'a2 -> 'a1 -> 'a2 **)
58 let rewrite_r x hx y =
61 (** val eq_coerc : 'a1 -> 'a2 **)
63 eq_rect_Type0 __ (Obj.magic ha) __
65 (** val true_rect_Type4 : 'a1 -> 'a1 **)
66 let rec true_rect_Type4 h_I =
69 (** val true_rect_Type5 : 'a1 -> 'a1 **)
70 let rec true_rect_Type5 h_I =
73 (** val true_rect_Type3 : 'a1 -> 'a1 **)
74 let rec true_rect_Type3 h_I =
77 (** val true_rect_Type2 : 'a1 -> 'a1 **)
78 let rec true_rect_Type2 h_I =
81 (** val true_rect_Type1 : 'a1 -> 'a1 **)
82 let rec true_rect_Type1 h_I =
85 (** val true_rect_Type0 : 'a1 -> 'a1 **)
86 let rec true_rect_Type0 h_I =
89 (** val true_inv_rect_Type4 : (__ -> 'a1) -> 'a1 **)
90 let true_inv_rect_Type4 h1 =
91 let hcut = true_rect_Type4 h1 in hcut __
93 (** val true_inv_rect_Type3 : (__ -> 'a1) -> 'a1 **)
94 let true_inv_rect_Type3 h1 =
95 let hcut = true_rect_Type3 h1 in hcut __
97 (** val true_inv_rect_Type2 : (__ -> 'a1) -> 'a1 **)
98 let true_inv_rect_Type2 h1 =
99 let hcut = true_rect_Type2 h1 in hcut __
101 (** val true_inv_rect_Type1 : (__ -> 'a1) -> 'a1 **)
102 let true_inv_rect_Type1 h1 =
103 let hcut = true_rect_Type1 h1 in hcut __
105 (** val true_inv_rect_Type0 : (__ -> 'a1) -> 'a1 **)
106 let true_inv_rect_Type0 h1 =
107 let hcut = true_rect_Type0 h1 in hcut __
109 (** val true_discr : __ -> __ **)
111 eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH)) __
113 (** val false_rect_Type4 : __ -> 'a1 **)
114 let rec false_rect_Type4 _ =
115 assert false (* absurd case *)
117 (** val false_rect_Type5 : __ -> 'a1 **)
118 let rec false_rect_Type5 _ =
119 assert false (* absurd case *)
121 (** val false_rect_Type3 : __ -> 'a1 **)
122 let rec false_rect_Type3 _ =
123 assert false (* absurd case *)
125 (** val false_rect_Type2 : __ -> 'a1 **)
126 let rec false_rect_Type2 _ =
127 assert false (* absurd case *)
129 (** val false_rect_Type1 : __ -> 'a1 **)
130 let rec false_rect_Type1 _ =
131 assert false (* absurd case *)
133 (** val false_rect_Type0 : __ -> 'a1 **)
134 let rec false_rect_Type0 _ =
135 assert false (* absurd case *)
137 (** val not_rect_Type4 : (__ -> 'a1) -> 'a1 **)
138 let rec not_rect_Type4 h_nmk =
141 (** val not_rect_Type5 : (__ -> 'a1) -> 'a1 **)
142 let rec not_rect_Type5 h_nmk =
145 (** val not_rect_Type3 : (__ -> 'a1) -> 'a1 **)
146 let rec not_rect_Type3 h_nmk =
149 (** val not_rect_Type2 : (__ -> 'a1) -> 'a1 **)
150 let rec not_rect_Type2 h_nmk =
153 (** val not_rect_Type1 : (__ -> 'a1) -> 'a1 **)
154 let rec not_rect_Type1 h_nmk =
157 (** val not_rect_Type0 : (__ -> 'a1) -> 'a1 **)
158 let rec not_rect_Type0 h_nmk =
161 (** val not_inv_rect_Type4 : (__ -> __ -> 'a1) -> 'a1 **)
162 let not_inv_rect_Type4 h1 =
163 let hcut = not_rect_Type4 h1 in hcut __
165 (** val not_inv_rect_Type3 : (__ -> __ -> 'a1) -> 'a1 **)
166 let not_inv_rect_Type3 h1 =
167 let hcut = not_rect_Type3 h1 in hcut __
169 (** val not_inv_rect_Type2 : (__ -> __ -> 'a1) -> 'a1 **)
170 let not_inv_rect_Type2 h1 =
171 let hcut = not_rect_Type2 h1 in hcut __
173 (** val not_inv_rect_Type1 : (__ -> __ -> 'a1) -> 'a1 **)
174 let not_inv_rect_Type1 h1 =
175 let hcut = not_rect_Type1 h1 in hcut __
177 (** val not_inv_rect_Type0 : (__ -> __ -> 'a1) -> 'a1 **)
178 let not_inv_rect_Type0 h1 =
179 let hcut = not_rect_Type0 h1 in hcut __
181 (** val and_rect_Type4 : (__ -> __ -> 'a1) -> 'a1 **)
182 let rec and_rect_Type4 h_conj =
185 (** val and_rect_Type5 : (__ -> __ -> 'a1) -> 'a1 **)
186 let rec and_rect_Type5 h_conj =
189 (** val and_rect_Type3 : (__ -> __ -> 'a1) -> 'a1 **)
190 let rec and_rect_Type3 h_conj =
193 (** val and_rect_Type2 : (__ -> __ -> 'a1) -> 'a1 **)
194 let rec and_rect_Type2 h_conj =
197 (** val and_rect_Type1 : (__ -> __ -> 'a1) -> 'a1 **)
198 let rec and_rect_Type1 h_conj =
201 (** val and_rect_Type0 : (__ -> __ -> 'a1) -> 'a1 **)
202 let rec and_rect_Type0 h_conj =
205 (** val and_inv_rect_Type4 : (__ -> __ -> __ -> 'a1) -> 'a1 **)
206 let and_inv_rect_Type4 h1 =
207 let hcut = and_rect_Type4 h1 in hcut __
209 (** val and_inv_rect_Type3 : (__ -> __ -> __ -> 'a1) -> 'a1 **)
210 let and_inv_rect_Type3 h1 =
211 let hcut = and_rect_Type3 h1 in hcut __
213 (** val and_inv_rect_Type2 : (__ -> __ -> __ -> 'a1) -> 'a1 **)
214 let and_inv_rect_Type2 h1 =
215 let hcut = and_rect_Type2 h1 in hcut __
217 (** val and_inv_rect_Type1 : (__ -> __ -> __ -> 'a1) -> 'a1 **)
218 let and_inv_rect_Type1 h1 =
219 let hcut = and_rect_Type1 h1 in hcut __
221 (** val and_inv_rect_Type0 : (__ -> __ -> __ -> 'a1) -> 'a1 **)
222 let and_inv_rect_Type0 h1 =
223 let hcut = and_rect_Type0 h1 in hcut __
225 (** val r0 : 'a1 -> 'a1 **)
229 (** val r1 : 'a1 -> 'a2 -> 'a1 -> 'a2 **)
230 let r1 x h_refl x_19 =
231 eq_rect_Type0 x h_refl x_19
233 (** val r2 : 'a1 -> 'a2 -> 'a3 -> 'a1 -> 'a2 -> 'a3 **)
234 let r2 a0 a1 a2 b0 b1 =
235 eq_rect_Type0 (r1 a0 a1 b0) (r1 a0 a2 b0) b1
237 (** val r3 : 'a1 -> 'a2 -> 'a3 -> 'a4 -> 'a1 -> 'a2 -> 'a3 -> 'a4 **)
238 let r3 a0 a1 a2 a3 b0 b1 b2 =
239 eq_rect_Type0 (r2 a0 a1 a2 b0 b1) (r2 a0 a1 a3 b0 b1) b2
242 'a1 -> 'a2 -> 'a3 -> 'a4 -> 'a5 -> 'a1 -> 'a2 -> 'a3 -> 'a4 -> 'a5 **)
243 let r4 a0 a1 a2 a3 a4 b0 b1 b2 b3 =
244 eq_rect_Type0 (r3 a0 a1 a2 a3 b0 b1 b2) (r3 a0 a1 a2 a4 b0 b1 b2) b3
246 (** val streicherK : 'a1 -> 'a2 -> 'a2 **)
248 eq_rect_Type3_r __ h __