13 (* singleton inductive, whose constructor was mk_Sigma *)
15 (** val sigma_rect_Type4 : (__ -> __ -> 'a1) -> sigma -> 'a1 **)
16 let rec sigma_rect_Type4 h_mk_Sigma x_812 =
17 let x_813 = x_812 in h_mk_Sigma __ x_813
19 (** val sigma_rect_Type5 : (__ -> __ -> 'a1) -> sigma -> 'a1 **)
20 let rec sigma_rect_Type5 h_mk_Sigma x_815 =
21 let x_816 = x_815 in h_mk_Sigma __ x_816
23 (** val sigma_rect_Type3 : (__ -> __ -> 'a1) -> sigma -> 'a1 **)
24 let rec sigma_rect_Type3 h_mk_Sigma x_818 =
25 let x_819 = x_818 in h_mk_Sigma __ x_819
27 (** val sigma_rect_Type2 : (__ -> __ -> 'a1) -> sigma -> 'a1 **)
28 let rec sigma_rect_Type2 h_mk_Sigma x_821 =
29 let x_822 = x_821 in h_mk_Sigma __ x_822
31 (** val sigma_rect_Type1 : (__ -> __ -> 'a1) -> sigma -> 'a1 **)
32 let rec sigma_rect_Type1 h_mk_Sigma x_824 =
33 let x_825 = x_824 in h_mk_Sigma __ x_825
35 (** val sigma_rect_Type0 : (__ -> __ -> 'a1) -> sigma -> 'a1 **)
36 let rec sigma_rect_Type0 h_mk_Sigma x_827 =
37 let x_828 = x_827 in h_mk_Sigma __ x_828
39 (** val sigma_inv_rect_Type4 : sigma -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
40 let sigma_inv_rect_Type4 hterm h1 =
41 let hcut = sigma_rect_Type4 h1 hterm in hcut __
43 (** val sigma_inv_rect_Type3 : sigma -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
44 let sigma_inv_rect_Type3 hterm h1 =
45 let hcut = sigma_rect_Type3 h1 hterm in hcut __
47 (** val sigma_inv_rect_Type2 : sigma -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
48 let sigma_inv_rect_Type2 hterm h1 =
49 let hcut = sigma_rect_Type2 h1 hterm in hcut __
51 (** val sigma_inv_rect_Type1 : sigma -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
52 let sigma_inv_rect_Type1 hterm h1 =
53 let hcut = sigma_rect_Type1 h1 hterm in hcut __
55 (** val sigma_inv_rect_Type0 : sigma -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
56 let sigma_inv_rect_Type0 hterm h1 =
57 let hcut = sigma_rect_Type0 h1 hterm in hcut __
61 (** val p2 : sigma -> p1 **)
65 (** val jmeq_rect_Type4 : 'a1 -> 'a2 -> 'a3 -> 'a2 **)
66 let rec jmeq_rect_Type4 x h_refl_jmeq x_851 =
69 (** val jmeq_rect_Type5 : 'a1 -> 'a2 -> 'a3 -> 'a2 **)
70 let rec jmeq_rect_Type5 x h_refl_jmeq x_854 =
73 (** val jmeq_rect_Type3 : 'a1 -> 'a2 -> 'a3 -> 'a2 **)
74 let rec jmeq_rect_Type3 x h_refl_jmeq x_857 =
77 (** val jmeq_rect_Type2 : 'a1 -> 'a2 -> 'a3 -> 'a2 **)
78 let rec jmeq_rect_Type2 x h_refl_jmeq x_860 =
81 (** val jmeq_rect_Type1 : 'a1 -> 'a2 -> 'a3 -> 'a2 **)
82 let rec jmeq_rect_Type1 x h_refl_jmeq x_863 =
85 (** val jmeq_rect_Type0 : 'a1 -> 'a2 -> 'a3 -> 'a2 **)
86 let rec jmeq_rect_Type0 x h_refl_jmeq x_866 =
89 (** val jmeq_inv_rect_Type4 : 'a1 -> 'a2 -> (__ -> __ -> 'a3) -> 'a3 **)
90 let jmeq_inv_rect_Type4 x2 x4 h1 =
91 let hcut = jmeq_rect_Type4 x2 h1 x4 in hcut __ __
93 (** val jmeq_inv_rect_Type3 : 'a1 -> 'a2 -> (__ -> __ -> 'a3) -> 'a3 **)
94 let jmeq_inv_rect_Type3 x2 x4 h1 =
95 let hcut = jmeq_rect_Type3 x2 h1 x4 in hcut __ __
97 (** val jmeq_inv_rect_Type2 : 'a1 -> 'a2 -> (__ -> __ -> 'a3) -> 'a3 **)
98 let jmeq_inv_rect_Type2 x2 x4 h1 =
99 let hcut = jmeq_rect_Type2 x2 h1 x4 in hcut __ __
101 (** val jmeq_inv_rect_Type1 : 'a1 -> 'a2 -> (__ -> __ -> 'a3) -> 'a3 **)
102 let jmeq_inv_rect_Type1 x2 x4 h1 =
103 let hcut = jmeq_rect_Type1 x2 h1 x4 in hcut __ __
105 (** val jmeq_inv_rect_Type0 : 'a1 -> 'a2 -> (__ -> __ -> 'a3) -> 'a3 **)
106 let jmeq_inv_rect_Type0 x2 x4 h1 =
107 let hcut = jmeq_rect_Type0 x2 h1 x4 in hcut __ __
109 (** val jmeq_discr : 'a1 -> 'a2 -> __ **)
110 let jmeq_discr a2 a4 =
111 Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH)) __
113 (** val cast : 'a1 -> 'a2 **)
115 (fun x0 -> Obj.magic x0) x
117 type ('a, 'x) curry = 'x
119 (** val g : 'a1 -> 'a2 -> 'a1 -> 'a2 **)
121 (fun _ -> Logic.eq_rect_Type0 __ h __) __
125 (** val e : 'a1 -> 'a2 pP -> 'a1 -> 'a2 pP **)
129 (** val jmeq_elim : 'a1 -> 'a2 -> 'a1 -> 'a2 **)
130 let jmeq_elim x x0 y =