17 val nat_rect_Type4 : 'a1 -> (nat -> 'a1 -> 'a1) -> nat -> 'a1
19 val nat_rect_Type3 : 'a1 -> (nat -> 'a1 -> 'a1) -> nat -> 'a1
21 val nat_rect_Type2 : 'a1 -> (nat -> 'a1 -> 'a1) -> nat -> 'a1
23 val nat_rect_Type1 : 'a1 -> (nat -> 'a1 -> 'a1) -> nat -> 'a1
25 val nat_rect_Type0 : 'a1 -> (nat -> 'a1 -> 'a1) -> nat -> 'a1
27 val nat_inv_rect_Type4 :
28 nat -> (__ -> 'a1) -> (nat -> (__ -> 'a1) -> __ -> 'a1) -> 'a1
30 val nat_inv_rect_Type3 :
31 nat -> (__ -> 'a1) -> (nat -> (__ -> 'a1) -> __ -> 'a1) -> 'a1
33 val nat_inv_rect_Type2 :
34 nat -> (__ -> 'a1) -> (nat -> (__ -> 'a1) -> __ -> 'a1) -> 'a1
36 val nat_inv_rect_Type1 :
37 nat -> (__ -> 'a1) -> (nat -> (__ -> 'a1) -> __ -> 'a1) -> 'a1
39 val nat_inv_rect_Type0 :
40 nat -> (__ -> 'a1) -> (nat -> (__ -> 'a1) -> __ -> 'a1) -> 'a1
42 val nat_discr : nat -> nat -> __
46 val plus : nat -> nat -> nat
48 val times : nat -> nat -> nat
50 val minus : nat -> nat -> nat
54 val eqb : nat -> nat -> Bool.bool
56 val leb : nat -> nat -> Bool.bool
58 val min : nat -> nat -> nat
60 val max : nat -> nat -> nat