29 (** val dAEMONXXX_rect_Type4 : 'a1 -> 'a1 -> dAEMONXXX -> 'a1 **)
30 let rec dAEMONXXX_rect_Type4 h_K1DAEMONXXX h_K2DAEMONXXX = function
31 | K1DAEMONXXX -> h_K1DAEMONXXX
32 | K2DAEMONXXX -> h_K2DAEMONXXX
34 (** val dAEMONXXX_rect_Type5 : 'a1 -> 'a1 -> dAEMONXXX -> 'a1 **)
35 let rec dAEMONXXX_rect_Type5 h_K1DAEMONXXX h_K2DAEMONXXX = function
36 | K1DAEMONXXX -> h_K1DAEMONXXX
37 | K2DAEMONXXX -> h_K2DAEMONXXX
39 (** val dAEMONXXX_rect_Type3 : 'a1 -> 'a1 -> dAEMONXXX -> 'a1 **)
40 let rec dAEMONXXX_rect_Type3 h_K1DAEMONXXX h_K2DAEMONXXX = function
41 | K1DAEMONXXX -> h_K1DAEMONXXX
42 | K2DAEMONXXX -> h_K2DAEMONXXX
44 (** val dAEMONXXX_rect_Type2 : 'a1 -> 'a1 -> dAEMONXXX -> 'a1 **)
45 let rec dAEMONXXX_rect_Type2 h_K1DAEMONXXX h_K2DAEMONXXX = function
46 | K1DAEMONXXX -> h_K1DAEMONXXX
47 | K2DAEMONXXX -> h_K2DAEMONXXX
49 (** val dAEMONXXX_rect_Type1 : 'a1 -> 'a1 -> dAEMONXXX -> 'a1 **)
50 let rec dAEMONXXX_rect_Type1 h_K1DAEMONXXX h_K2DAEMONXXX = function
51 | K1DAEMONXXX -> h_K1DAEMONXXX
52 | K2DAEMONXXX -> h_K2DAEMONXXX
54 (** val dAEMONXXX_rect_Type0 : 'a1 -> 'a1 -> dAEMONXXX -> 'a1 **)
55 let rec dAEMONXXX_rect_Type0 h_K1DAEMONXXX h_K2DAEMONXXX = function
56 | K1DAEMONXXX -> h_K1DAEMONXXX
57 | K2DAEMONXXX -> h_K2DAEMONXXX
59 (** val dAEMONXXX_inv_rect_Type4 :
60 dAEMONXXX -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
61 let dAEMONXXX_inv_rect_Type4 hterm h1 h2 =
62 let hcut = dAEMONXXX_rect_Type4 h1 h2 hterm in hcut __
64 (** val dAEMONXXX_inv_rect_Type3 :
65 dAEMONXXX -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
66 let dAEMONXXX_inv_rect_Type3 hterm h1 h2 =
67 let hcut = dAEMONXXX_rect_Type3 h1 h2 hterm in hcut __
69 (** val dAEMONXXX_inv_rect_Type2 :
70 dAEMONXXX -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
71 let dAEMONXXX_inv_rect_Type2 hterm h1 h2 =
72 let hcut = dAEMONXXX_rect_Type2 h1 h2 hterm in hcut __
74 (** val dAEMONXXX_inv_rect_Type1 :
75 dAEMONXXX -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
76 let dAEMONXXX_inv_rect_Type1 hterm h1 h2 =
77 let hcut = dAEMONXXX_rect_Type1 h1 h2 hterm in hcut __
79 (** val dAEMONXXX_inv_rect_Type0 :
80 dAEMONXXX -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
81 let dAEMONXXX_inv_rect_Type0 hterm h1 h2 =
82 let hcut = dAEMONXXX_rect_Type0 h1 h2 hterm in hcut __
84 (** val dAEMONXXX_discr : dAEMONXXX -> dAEMONXXX -> __ **)
85 let dAEMONXXX_discr x y =
88 | K1DAEMONXXX -> Obj.magic (fun _ dH -> dH)
89 | K2DAEMONXXX -> Obj.magic (fun _ dH -> dH)) y
91 (** val dAEMONXXX_jmdiscr : dAEMONXXX -> dAEMONXXX -> __ **)
92 let dAEMONXXX_jmdiscr x y =
95 | K1DAEMONXXX -> Obj.magic (fun _ dH -> dH)
96 | K2DAEMONXXX -> Obj.magic (fun _ dH -> dH)) y
98 (** val ltb : Nat.nat -> Nat.nat -> Bool.bool **)
102 (** val geb : Nat.nat -> Nat.nat -> Bool.bool **)
106 (** val gtb : Nat.nat -> Nat.nat -> Bool.bool **)
110 (** val eq_nat : Nat.nat -> Nat.nat -> Bool.bool **)
116 | Nat.S x -> Bool.False)
119 | Nat.O -> Bool.False
120 | Nat.S m' -> eq_nat n' m')
122 (** val forall : ('a1 -> Bool.bool) -> 'a1 List.list -> Bool.bool **)
123 let rec forall f = function
124 | List.Nil -> Bool.True
125 | List.Cons (hd, tl) -> Bool.andb (f hd) (forall f tl)
127 (** val prefix : Nat.nat -> 'a1 List.list -> 'a1 List.list **)
128 let rec prefix k = function
129 | List.Nil -> List.Nil
130 | List.Cons (hd, tl) ->
133 | Nat.S k' -> List.Cons (hd, (prefix k' tl)))
136 ('a1 -> 'a2 -> 'a3 -> 'a1) -> 'a1 -> 'a2 List.list -> 'a3 List.list ->
138 let rec fold_left2 f accu left right =
143 | List.Nil -> (fun _ -> accu)
144 | List.Cons (hd, tl) ->
146 Obj.magic Nat.nat_discr Nat.O (Nat.S (List.length tl)) __)) __)
147 | List.Cons (hd, tl) ->
152 Obj.magic Nat.nat_discr (Nat.S (List.length tl)) Nat.O __)
153 | List.Cons (hd', tl') ->
154 (fun _ -> fold_left2 f (f accu hd hd') tl tl')) __)) __
156 (** val remove_n_first_internal :
157 Nat.nat -> 'a1 List.list -> Nat.nat -> 'a1 List.list **)
158 let rec remove_n_first_internal i l n =
160 | List.Nil -> List.Nil
161 | List.Cons (hd, tl) ->
162 (match eq_nat i n with
164 | Bool.False -> remove_n_first_internal (Nat.S i) tl n)
166 (** val remove_n_first : Nat.nat -> 'a1 List.list -> 'a1 List.list **)
167 let remove_n_first n l =
168 remove_n_first_internal Nat.O l n
170 (** val foldi_from_until_internal :
171 Nat.nat -> 'a1 List.list -> 'a1 List.list -> Nat.nat -> (Nat.nat -> 'a1
172 List.list -> 'a1 -> 'a1 List.list) -> 'a1 List.list **)
173 let rec foldi_from_until_internal i res rem m f =
176 | List.Cons (e, tl) ->
179 | Bool.False -> foldi_from_until_internal (Nat.S i) (f i res e) tl m f)
181 (** val foldi_from_until :
182 Nat.nat -> Nat.nat -> (Nat.nat -> 'a1 List.list -> 'a1 -> 'a1 List.list)
183 -> 'a1 List.list -> 'a1 List.list -> 'a1 List.list **)
184 let foldi_from_until n m f a l =
185 foldi_from_until_internal Nat.O a (remove_n_first n l) m f
188 Nat.nat -> (Nat.nat -> 'a1 List.list -> 'a1 -> 'a1 List.list) -> 'a1
189 List.list -> 'a1 List.list -> 'a1 List.list **)
190 let foldi_from n f a l =
191 foldi_from_until n (List.length l) f a l
193 (** val foldi_until :
194 Nat.nat -> (Nat.nat -> 'a1 List.list -> 'a1 -> 'a1 List.list) -> 'a1
195 List.list -> 'a1 List.list -> 'a1 List.list **)
196 let foldi_until m f a l =
197 foldi_from_until Nat.O m f a l
200 (Nat.nat -> 'a1 List.list -> 'a1 -> 'a1 List.list) -> 'a1 List.list ->
201 'a1 List.list -> 'a1 List.list **)
203 foldi_from_until Nat.O (List.length l) f a l
205 (** val hd_safe : 'a1 List.list -> 'a1 **)
208 | List.Nil -> (fun _ -> assert false (* absurd case *))
209 | List.Cons (hd, tl) -> (fun _ -> hd)) __
211 (** val tail_safe : 'a1 List.list -> 'a1 List.list **)
214 | List.Nil -> (fun _ -> assert false (* absurd case *))
215 | List.Cons (hd, tl) -> (fun _ -> tl)) __
218 'a1 List.list -> Nat.nat -> ('a1 List.list, 'a1 List.list) Types.prod **)
219 let rec safe_split l index =
221 | Nat.O -> (fun _ -> { Types.fst = List.Nil; Types.snd = l })
225 | List.Nil -> (fun _ -> assert false (* absurd case *))
226 | List.Cons (hd, tl) ->
228 let { Types.fst = l1; Types.snd = l2 } = safe_split tl index' in
229 { Types.fst = (List.Cons (hd, l1)); Types.snd = l2 })) __)) __
231 (** val nth_safe : Nat.nat -> 'a1 List.list -> 'a1 **)
232 let rec nth_safe index the_list =
236 | List.Nil -> (fun _ -> Logic.false_rect_Type0 __)
237 | List.Cons (hd, tl) -> (fun _ -> hd))
240 | List.Nil -> (fun _ -> Logic.false_rect_Type0 __)
241 | List.Cons (hd, tl) -> (fun _ -> nth_safe index' tl))) __
243 (** val last_safe : 'a1 List.list -> 'a1 **)
244 let last_safe the_list =
245 nth_safe (Nat.minus (List.length the_list) (Nat.S Nat.O)) the_list
248 'a1 List.list -> 'a2 List.list -> (('a1 List.list, 'a1 List.list)
249 Types.prod, ('a2 List.list, 'a2 List.list) Types.prod) Types.prod **)
250 let rec reduce left right =
253 { Types.fst = { Types.fst = List.Nil; Types.snd = List.Nil }; Types.snd =
254 { Types.fst = List.Nil; Types.snd = right } }
255 | List.Cons (hd, tl) ->
258 { Types.fst = { Types.fst = List.Nil; Types.snd = left }; Types.snd =
259 { Types.fst = List.Nil; Types.snd = List.Nil } }
260 | List.Cons (hd', tl') ->
261 let { Types.fst = cleft; Types.snd = cright } = reduce tl tl' in
262 let { Types.fst = commonl; Types.snd = restl } = cleft in
263 let { Types.fst = commonr; Types.snd = restr } = cright in
264 { Types.fst = { Types.fst = (List.Cons (hd, commonl)); Types.snd =
265 restl }; Types.snd = { Types.fst = (List.Cons (hd', commonr));
266 Types.snd = restr } })
268 (** val reduce_strong :
269 'a1 List.list -> 'a2 List.list -> (('a1 List.list, 'a1 List.list)
270 Types.prod, ('a2 List.list, 'a2 List.list) Types.prod) Types.prod
272 let rec reduce_strong left right =
275 (fun _ -> { Types.fst = { Types.fst = List.Nil; Types.snd = List.Nil };
276 Types.snd = { Types.fst = List.Nil; Types.snd = right } })
277 | List.Cons (hd, tl) ->
281 (fun _ -> { Types.fst = { Types.fst = List.Nil; Types.snd = left };
282 Types.snd = { Types.fst = List.Nil; Types.snd = List.Nil } })
283 | List.Cons (hd', tl') ->
285 (let { Types.fst = cleft; Types.snd = cright } =
286 Types.pi1 (reduce_strong tl tl')
289 (let { Types.fst = commonl; Types.snd = restl } = cleft in
291 (let { Types.fst = commonr; Types.snd = restr } = cright in
292 (fun _ -> { Types.fst = { Types.fst = (List.Cons (hd, commonl));
293 Types.snd = restl }; Types.snd = { Types.fst = (List.Cons (hd',
294 commonr)); Types.snd = restr } })) __)) __)) __)) __)) __
297 ('a1 -> 'a2 -> 'a3) -> 'a1 List.list -> 'a2 List.list -> 'a3 List.list
299 let rec map2_opt f left right =
303 | List.Nil -> Types.Some List.Nil
304 | List.Cons (x, x0) -> Types.None)
305 | List.Cons (hd, tl) ->
307 | List.Nil -> Types.None
308 | List.Cons (hd', tl') ->
309 (match map2_opt f tl tl' with
310 | Types.None -> Types.None
311 | Types.Some tail -> Types.Some (List.Cons ((f hd hd'), tail))))
314 ('a1 -> 'a2 -> 'a3) -> 'a1 List.list -> 'a2 List.list -> 'a3 List.list **)
315 let rec map2 f left right =
319 | List.Nil -> (fun _ -> List.Nil)
320 | List.Cons (x, x0) ->
321 (fun _ -> Obj.magic Nat.nat_discr Nat.O (Nat.S (List.length x0)) __))
322 | List.Cons (hd, tl) ->
325 (fun _ -> Obj.magic Nat.nat_discr (Nat.S (List.length tl)) Nat.O __)
326 | List.Cons (hd', tl') ->
327 (fun _ -> List.Cons ((f hd hd'), (map2 f tl tl'))))) __
330 ('a1 -> 'a2 -> 'a3 -> 'a4) -> 'a1 List.list -> 'a2 List.list -> 'a3
331 List.list -> 'a4 List.list **)
332 let rec map3 f left centre right =
340 | List.Nil -> (fun _ -> List.Nil)
341 | List.Cons (hd, tl) ->
343 Obj.magic Nat.nat_discr Nat.O (Nat.S (List.length tl)) __))
345 | List.Cons (hd, tl) ->
347 Logic.eq_rect_Type0 (List.length centre)
348 (Logic.eq_rect_Type0 (List.length List.Nil) (fun _ ->
349 Obj.magic Nat.nat_discr (Nat.S (List.length tl)) Nat.O __)
350 (List.length centre)) (List.length right) __)) __)
351 | List.Cons (hd, tl) ->
356 Logic.eq_rect_Type0 (List.length centre)
357 (Logic.eq_rect_Type0 (List.length (List.Cons (hd, tl)))
359 Obj.magic Nat.nat_discr Nat.O (Nat.S (List.length tl)) __)
360 (List.length centre)) (List.length right) __)
361 | List.Cons (hd', tl') ->
366 Obj.magic Nat.nat_discr (Nat.S (List.length tl')) Nat.O __)
367 | List.Cons (hd'', tl'') ->
368 (fun _ _ -> List.Cons ((f hd hd' hd''), (map3 f tl tl' tl''))))
371 (** val eq_rect_Type0_r : 'a1 -> 'a2 -> 'a1 -> 'a2 **)
372 let eq_rect_Type0_r a h x =
373 (fun _ auto -> auto) __ h
375 (** val safe_nth : Nat.nat -> 'a1 List.list -> 'a1 **)
376 let rec safe_nth n l =
380 | List.Nil -> (fun _ -> Logic.false_rect_Type0 __)
381 | List.Cons (hd, tl) -> (fun _ -> hd))
384 | List.Nil -> (fun _ -> Logic.false_rect_Type0 __)
385 | List.Cons (hd, tl) -> (fun _ -> safe_nth n' tl))) __
387 (** val nub_by_internal :
388 ('a1 -> 'a1 -> Bool.bool) -> 'a1 List.list -> Nat.nat -> 'a1 List.list **)
389 let rec nub_by_internal f l = function
392 | List.Nil -> List.Nil
393 | List.Cons (hd, tl) -> l)
396 | List.Nil -> List.Nil
397 | List.Cons (hd, tl) ->
399 (nub_by_internal f (List.filter (fun y -> Bool.notb (f y hd)) tl) n0)))
402 ('a1 -> 'a1 -> Bool.bool) -> 'a1 List.list -> 'a1 List.list **)
404 nub_by_internal f l (List.length l)
407 ('a1 -> 'a1 -> Bool.bool) -> 'a1 -> 'a1 List.list -> Bool.bool **)
408 let rec member eq a = function
409 | List.Nil -> Bool.False
410 | List.Cons (hd, tl) -> Bool.orb (eq a hd) (member eq a tl)
412 (** val take : Nat.nat -> 'a1 List.list -> 'a1 List.list **)
418 | List.Nil -> List.Nil
419 | List.Cons (hd, tl) -> List.Cons (hd, (take n0 tl)))
421 (** val drop : Nat.nat -> 'a1 List.list -> 'a1 List.list **)
427 | List.Nil -> List.Nil
428 | List.Cons (hd, tl) -> drop n0 tl)
431 Nat.nat -> 'a1 List.list -> ('a1 List.list, 'a1 List.list) Types.prod **)
433 { Types.fst = (take n l); Types.snd = (drop n l) }
435 (** val mapi_internal :
436 Nat.nat -> (Nat.nat -> 'a1 -> 'a2) -> 'a1 List.list -> 'a2 List.list **)
437 let rec mapi_internal n f = function
438 | List.Nil -> List.Nil
439 | List.Cons (hd, tl) ->
440 List.Cons ((f n hd), (mapi_internal (Nat.plus n (Nat.S Nat.O)) f tl))
442 (** val mapi : (Nat.nat -> 'a1 -> 'a2) -> 'a1 List.list -> 'a2 List.list **)
444 mapi_internal Nat.O f l
446 (** val zip_pottier :
447 'a1 List.list -> 'a2 List.list -> ('a1, 'a2) Types.prod List.list **)
448 let rec zip_pottier left right =
450 | List.Nil -> List.Nil
451 | List.Cons (hd, tl) ->
453 | List.Nil -> List.Nil
454 | List.Cons (hd', tl') ->
455 List.Cons ({ Types.fst = hd; Types.snd = hd' }, (zip_pottier tl tl')))
458 'a1 List.list -> 'a2 List.list -> ('a1, 'a2) Types.prod List.list **)
459 let rec zip_safe left right =
464 | List.Nil -> (fun _ -> List.Nil)
465 | List.Cons (hd, tl) ->
467 Obj.magic Nat.nat_discr Nat.O (Nat.S (List.length tl)) __)) __)
468 | List.Cons (hd, tl) ->
473 Obj.magic Nat.nat_discr (Nat.S (List.length tl)) Nat.O __)
474 | List.Cons (hd', tl') ->
475 (fun _ -> List.Cons ({ Types.fst = hd; Types.snd = hd' },
476 (zip_safe tl tl')))) __)) __
479 'a1 List.list -> 'a2 List.list -> ('a1, 'a2) Types.prod List.list
483 | List.Nil -> Types.Some List.Nil
484 | List.Cons (hd, tl) ->
486 | List.Nil -> Types.None
487 | List.Cons (hd', tl') ->
488 (match zip tl tl' with
489 | Types.None -> Types.None
491 Types.Some (List.Cons ({ Types.fst = hd; Types.snd = hd' }, tail))))
493 (** val foldl : ('a1 -> 'a2 -> 'a1) -> 'a1 -> 'a2 List.list -> 'a1 **)
494 let rec foldl f a = function
496 | List.Cons (hd, tl) -> foldl f (f a hd) tl
498 (** val rev : 'a1 List.list -> 'a1 List.list **)
502 (** val fold_left_i_aux :
503 (Nat.nat -> 'a1 -> 'a2 -> 'a1) -> 'a1 -> Nat.nat -> 'a2 List.list -> 'a1 **)
504 let rec fold_left_i_aux f x i = function
506 | List.Cons (hd, tl) -> fold_left_i_aux f (f i x hd) (Nat.S i) tl
508 (** val fold_left_i :
509 (Nat.nat -> 'a1 -> 'a2 -> 'a1) -> 'a1 -> 'a2 List.list -> 'a1 **)
510 let fold_left_i f x =
511 fold_left_i_aux f x Nat.O
513 (** val function_apply : ('a1 -> 'a2) -> 'a1 -> 'a2 **)
514 let function_apply f a =
517 (** val iterate : ('a1 -> 'a1) -> 'a1 -> Nat.nat -> 'a1 **)
518 let rec iterate f a = function
520 | Nat.S o -> f (iterate f a o)
522 (** val division_aux : Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat **)
523 let rec division_aux m n p =
524 match ltb n (Nat.S p) with
529 | Nat.S q -> Nat.S (division_aux q (Nat.minus n (Nat.S p)) p))
531 (** val division : Nat.nat -> Nat.nat -> Nat.nat **)
532 let division m = function
534 | Nat.S o -> division_aux m m o
536 (** val modulus_aux : Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat **)
537 let rec modulus_aux m n p =
538 match Nat.leb n p with
543 | Nat.S o -> modulus_aux o (Nat.minus n (Nat.S p)) p)
545 (** val modulus : Nat.nat -> Nat.nat -> Nat.nat **)
546 let modulus m = function
548 | Nat.S o -> modulus_aux m m o
550 (** val divide_with_remainder :
551 Nat.nat -> Nat.nat -> (Nat.nat, Nat.nat) Types.prod **)
552 let divide_with_remainder m n =
553 { Types.fst = (division m n); Types.snd = (modulus m n) }
555 (** val less_than_or_equal_b_elim :
556 Nat.nat -> Nat.nat -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
557 let less_than_or_equal_b_elim m n h1 h2 =
558 (match Nat.leb m n with
559 | Bool.True -> (fun _ _ -> h1 __)
560 | Bool.False -> (fun _ _ -> h2 __)) __ __
564 (** val dpi1__o__bool_to_Prop__o__inject :
565 (Bool.bool, 'a1) Types.dPair -> __ Types.sig0 **)
566 let dpi1__o__bool_to_Prop__o__inject x2 =
569 (** val eject__o__bool_to_Prop__o__inject :
570 Bool.bool Types.sig0 -> __ Types.sig0 **)
571 let eject__o__bool_to_Prop__o__inject x2 =
574 (** val bool_to_Prop__o__inject : Bool.bool -> __ Types.sig0 **)
575 let bool_to_Prop__o__inject x1 =
578 (** val dpi1__o__bool_to_Prop_to_eq__o__inject :
579 Bool.bool -> (__, 'a1) Types.dPair -> __ Types.sig0 **)
580 let dpi1__o__bool_to_Prop_to_eq__o__inject x0 x3 =
583 (** val eject__o__bool_to_Prop_to_eq__o__inject :
584 Bool.bool -> __ Types.sig0 -> __ Types.sig0 **)
585 let eject__o__bool_to_Prop_to_eq__o__inject x0 x3 =
588 (** val bool_to_Prop_to_eq__o__inject : Bool.bool -> __ Types.sig0 **)
589 let bool_to_Prop_to_eq__o__inject x0 =
592 (** val dpi1__o__not_bool_to_Prop_to_eq__o__inject :
593 Bool.bool -> (__, 'a1) Types.dPair -> __ Types.sig0 **)
594 let dpi1__o__not_bool_to_Prop_to_eq__o__inject x0 x3 =
597 (** val eject__o__not_bool_to_Prop_to_eq__o__inject :
598 Bool.bool -> __ Types.sig0 -> __ Types.sig0 **)
599 let eject__o__not_bool_to_Prop_to_eq__o__inject x0 x3 =
602 (** val not_bool_to_Prop_to_eq__o__inject : Bool.bool -> __ Types.sig0 **)
603 let not_bool_to_Prop_to_eq__o__inject x0 =
606 (** val if_then_else_safe :
607 Bool.bool -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
608 let if_then_else_safe b f g =
611 | Bool.False -> g) __
613 (** val dpi1__o__not_neq_None__o__inject :
614 'a1 Types.option -> (__, 'a2) Types.dPair -> __ Types.sig0 **)
615 let dpi1__o__not_neq_None__o__inject x1 x4 =
618 (** val eject__o__not_neq_None__o__inject :
619 'a1 Types.option -> __ Types.sig0 -> __ Types.sig0 **)
620 let eject__o__not_neq_None__o__inject x1 x4 =
623 (** val not_neq_None__o__inject : 'a1 Types.option -> __ Types.sig0 **)
624 let not_neq_None__o__inject x1 =
627 (** val prod_jmdiscr :
628 ('a1, 'a2) Types.prod -> ('a1, 'a2) Types.prod -> __ **)
629 let prod_jmdiscr x y =
630 Logic.eq_rect_Type2 x
631 (let { Types.fst = a0; Types.snd = a10 } = x in
632 Obj.magic (fun _ dH -> dH __ __)) y
634 (** val eq_rect_Type1_r : 'a1 -> 'a2 -> 'a1 -> 'a2 **)
635 let eq_rect_Type1_r a h x =
636 (fun _ auto -> auto) __ h
638 (** val some_Some_elim : 'a1 -> 'a1 -> (__ -> 'a2) -> 'a2 **)
639 let some_Some_elim x y h =
642 (** val pose : 'a1 -> ('a1 -> __ -> 'a2) -> 'a2 **)
647 ('a1 -> 'a1 -> Bool.bool) -> ('a2 -> 'a2 -> Bool.bool) -> ('a1, 'a2)
648 Types.sum -> ('a1, 'a2) Types.sum -> Bool.bool **)
649 let eq_sum leq req left right =
653 | Types.Inl l' -> leq l l'
654 | Types.Inr x -> Bool.False)
657 | Types.Inl x -> Bool.False
658 | Types.Inr r' -> req r r')
661 ('a1 -> 'a1 -> Bool.bool) -> ('a2 -> 'a2 -> Bool.bool) -> ('a1, 'a2)
662 Types.prod -> ('a1, 'a2) Types.prod -> Bool.bool **)
663 let eq_prod leq req left right =
664 let { Types.fst = l; Types.snd = r } = left in
665 let { Types.fst = l'; Types.snd = r' } = right in
666 Bool.andb (leq l l') (req r r')