17 (** val nat_rect_Type4 : 'a1 -> (nat -> 'a1 -> 'a1) -> nat -> 'a1 **)
18 let rec nat_rect_Type4 h_O h_S = function
20 | S x_565 -> h_S x_565 (nat_rect_Type4 h_O h_S x_565)
22 (** val nat_rect_Type3 : 'a1 -> (nat -> 'a1 -> 'a1) -> nat -> 'a1 **)
23 let rec nat_rect_Type3 h_O h_S = function
25 | S x_573 -> h_S x_573 (nat_rect_Type3 h_O h_S x_573)
27 (** val nat_rect_Type2 : 'a1 -> (nat -> 'a1 -> 'a1) -> nat -> 'a1 **)
28 let rec nat_rect_Type2 h_O h_S = function
30 | S x_577 -> h_S x_577 (nat_rect_Type2 h_O h_S x_577)
32 (** val nat_rect_Type1 : 'a1 -> (nat -> 'a1 -> 'a1) -> nat -> 'a1 **)
33 let rec nat_rect_Type1 h_O h_S = function
35 | S x_581 -> h_S x_581 (nat_rect_Type1 h_O h_S x_581)
37 (** val nat_rect_Type0 : 'a1 -> (nat -> 'a1 -> 'a1) -> nat -> 'a1 **)
38 let rec nat_rect_Type0 h_O h_S = function
40 | S x_585 -> h_S x_585 (nat_rect_Type0 h_O h_S x_585)
42 (** val nat_inv_rect_Type4 :
43 nat -> (__ -> 'a1) -> (nat -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
44 let nat_inv_rect_Type4 hterm h1 h2 =
45 let hcut = nat_rect_Type4 h1 h2 hterm in hcut __
47 (** val nat_inv_rect_Type3 :
48 nat -> (__ -> 'a1) -> (nat -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
49 let nat_inv_rect_Type3 hterm h1 h2 =
50 let hcut = nat_rect_Type3 h1 h2 hterm in hcut __
52 (** val nat_inv_rect_Type2 :
53 nat -> (__ -> 'a1) -> (nat -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
54 let nat_inv_rect_Type2 hterm h1 h2 =
55 let hcut = nat_rect_Type2 h1 h2 hterm in hcut __
57 (** val nat_inv_rect_Type1 :
58 nat -> (__ -> 'a1) -> (nat -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
59 let nat_inv_rect_Type1 hterm h1 h2 =
60 let hcut = nat_rect_Type1 h1 h2 hterm in hcut __
62 (** val nat_inv_rect_Type0 :
63 nat -> (__ -> 'a1) -> (nat -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
64 let nat_inv_rect_Type0 hterm h1 h2 =
65 let hcut = nat_rect_Type0 h1 h2 hterm in hcut __
67 (** val nat_discr : nat -> nat -> __ **)
71 | O -> Obj.magic (fun _ dH -> dH)
72 | S a0 -> Obj.magic (fun _ dH -> dH __)) y
74 (** val pred : nat -> nat **)
79 (** val plus : nat -> nat -> nat **)
85 (** val times : nat -> nat -> nat **)
89 | S p -> plus m (times p m)
91 (** val minus : nat -> nat -> nat **)
102 (** val eqb : nat -> nat -> Bool.bool **)
114 (** val leb : nat -> nat -> Bool.bool **)
123 (** val min : nat -> nat -> nat **)
129 (** val max : nat -> nat -> nat **)