13 (* singleton inductive, whose constructor was mk_Sigma *)
15 val sigma_rect_Type4 : (__ -> __ -> 'a1) -> sigma -> 'a1
17 val sigma_rect_Type5 : (__ -> __ -> 'a1) -> sigma -> 'a1
19 val sigma_rect_Type3 : (__ -> __ -> 'a1) -> sigma -> 'a1
21 val sigma_rect_Type2 : (__ -> __ -> 'a1) -> sigma -> 'a1
23 val sigma_rect_Type1 : (__ -> __ -> 'a1) -> sigma -> 'a1
25 val sigma_rect_Type0 : (__ -> __ -> 'a1) -> sigma -> 'a1
27 val sigma_inv_rect_Type4 : sigma -> (__ -> __ -> __ -> 'a1) -> 'a1
29 val sigma_inv_rect_Type3 : sigma -> (__ -> __ -> __ -> 'a1) -> 'a1
31 val sigma_inv_rect_Type2 : sigma -> (__ -> __ -> __ -> 'a1) -> 'a1
33 val sigma_inv_rect_Type1 : sigma -> (__ -> __ -> __ -> 'a1) -> 'a1
35 val sigma_inv_rect_Type0 : sigma -> (__ -> __ -> __ -> 'a1) -> 'a1
41 val jmeq_rect_Type4 : 'a1 -> 'a2 -> 'a3 -> 'a2
43 val jmeq_rect_Type5 : 'a1 -> 'a2 -> 'a3 -> 'a2
45 val jmeq_rect_Type3 : 'a1 -> 'a2 -> 'a3 -> 'a2
47 val jmeq_rect_Type2 : 'a1 -> 'a2 -> 'a3 -> 'a2
49 val jmeq_rect_Type1 : 'a1 -> 'a2 -> 'a3 -> 'a2
51 val jmeq_rect_Type0 : 'a1 -> 'a2 -> 'a3 -> 'a2
53 val jmeq_inv_rect_Type4 : 'a1 -> 'a2 -> (__ -> __ -> 'a3) -> 'a3
55 val jmeq_inv_rect_Type3 : 'a1 -> 'a2 -> (__ -> __ -> 'a3) -> 'a3
57 val jmeq_inv_rect_Type2 : 'a1 -> 'a2 -> (__ -> __ -> 'a3) -> 'a3
59 val jmeq_inv_rect_Type1 : 'a1 -> 'a2 -> (__ -> __ -> 'a3) -> 'a3
61 val jmeq_inv_rect_Type0 : 'a1 -> 'a2 -> (__ -> __ -> 'a3) -> 'a3
63 val jmeq_discr : 'a1 -> 'a2 -> __
67 type ('a, 'x) curry = 'x
69 val g : 'a1 -> 'a2 -> 'a1 -> 'a2
73 val e : 'a1 -> 'a2 pP -> 'a1 -> 'a2 pP
75 val jmeq_elim : 'a1 -> 'a2 -> 'a1 -> 'a2