9 val eq_rect_Type4 : 'a1 -> 'a2 -> 'a1 -> 'a2
11 val eq_rect_Type5 : 'a1 -> 'a2 -> 'a1 -> 'a2
13 val eq_rect_Type3 : 'a1 -> 'a2 -> 'a1 -> 'a2
15 val eq_rect_Type2 : 'a1 -> 'a2 -> 'a1 -> 'a2
17 val eq_rect_Type1 : 'a1 -> 'a2 -> 'a1 -> 'a2
19 val eq_rect_Type0 : 'a1 -> 'a2 -> 'a1 -> 'a2
21 val eq_rect_r : 'a1 -> 'a1 -> 'a2 -> 'a2
23 val eq_rect_Type0_r : 'a1 -> 'a2 -> 'a1 -> 'a2
25 val eq_rect_Type1_r : 'a1 -> 'a2 -> 'a1 -> 'a2
27 val eq_rect_Type2_r : 'a1 -> 'a2 -> 'a1 -> 'a2
29 val eq_rect_Type3_r : 'a1 -> 'a2 -> 'a1 -> 'a2
31 val rewrite_l : 'a1 -> 'a2 -> 'a1 -> 'a2
33 val rewrite_r : 'a1 -> 'a2 -> 'a1 -> 'a2
35 val eq_coerc : 'a1 -> 'a2
37 val true_rect_Type4 : 'a1 -> 'a1
39 val true_rect_Type5 : 'a1 -> 'a1
41 val true_rect_Type3 : 'a1 -> 'a1
43 val true_rect_Type2 : 'a1 -> 'a1
45 val true_rect_Type1 : 'a1 -> 'a1
47 val true_rect_Type0 : 'a1 -> 'a1
49 val true_inv_rect_Type4 : (__ -> 'a1) -> 'a1
51 val true_inv_rect_Type3 : (__ -> 'a1) -> 'a1
53 val true_inv_rect_Type2 : (__ -> 'a1) -> 'a1
55 val true_inv_rect_Type1 : (__ -> 'a1) -> 'a1
57 val true_inv_rect_Type0 : (__ -> 'a1) -> 'a1
59 val true_discr : __ -> __
61 val false_rect_Type4 : __ -> 'a1
63 val false_rect_Type5 : __ -> 'a1
65 val false_rect_Type3 : __ -> 'a1
67 val false_rect_Type2 : __ -> 'a1
69 val false_rect_Type1 : __ -> 'a1
71 val false_rect_Type0 : __ -> 'a1
73 val not_rect_Type4 : (__ -> 'a1) -> 'a1
75 val not_rect_Type5 : (__ -> 'a1) -> 'a1
77 val not_rect_Type3 : (__ -> 'a1) -> 'a1
79 val not_rect_Type2 : (__ -> 'a1) -> 'a1
81 val not_rect_Type1 : (__ -> 'a1) -> 'a1
83 val not_rect_Type0 : (__ -> 'a1) -> 'a1
85 val not_inv_rect_Type4 : (__ -> __ -> 'a1) -> 'a1
87 val not_inv_rect_Type3 : (__ -> __ -> 'a1) -> 'a1
89 val not_inv_rect_Type2 : (__ -> __ -> 'a1) -> 'a1
91 val not_inv_rect_Type1 : (__ -> __ -> 'a1) -> 'a1
93 val not_inv_rect_Type0 : (__ -> __ -> 'a1) -> 'a1
95 val and_rect_Type4 : (__ -> __ -> 'a1) -> 'a1
97 val and_rect_Type5 : (__ -> __ -> 'a1) -> 'a1
99 val and_rect_Type3 : (__ -> __ -> 'a1) -> 'a1
101 val and_rect_Type2 : (__ -> __ -> 'a1) -> 'a1
103 val and_rect_Type1 : (__ -> __ -> 'a1) -> 'a1
105 val and_rect_Type0 : (__ -> __ -> 'a1) -> 'a1
107 val and_inv_rect_Type4 : (__ -> __ -> __ -> 'a1) -> 'a1
109 val and_inv_rect_Type3 : (__ -> __ -> __ -> 'a1) -> 'a1
111 val and_inv_rect_Type2 : (__ -> __ -> __ -> 'a1) -> 'a1
113 val and_inv_rect_Type1 : (__ -> __ -> __ -> 'a1) -> 'a1
115 val and_inv_rect_Type0 : (__ -> __ -> __ -> 'a1) -> 'a1
119 val r1 : 'a1 -> 'a2 -> 'a1 -> 'a2
121 val r2 : 'a1 -> 'a2 -> 'a3 -> 'a1 -> 'a2 -> 'a3
123 val r3 : 'a1 -> 'a2 -> 'a3 -> 'a4 -> 'a1 -> 'a2 -> 'a3 -> 'a4
125 val r4 : 'a1 -> 'a2 -> 'a3 -> 'a4 -> 'a5 -> 'a1 -> 'a2 -> 'a3 -> 'a4 -> 'a5
127 val streicherK : 'a1 -> 'a2 -> 'a2