extracted/types.ml

   1 open Preamble
   2
   3 open Hints_declaration
   4
   5 open Core_notation
   6
   7 open Pts
   8
   9 open Logic
  10
  11 type void = unit (* empty inductive *)
  12
  13 (** val void_rect_Type4 : void -> 'a1 **)
  14 let rec void_rect_Type4 x_327 =
  15   assert false (* absurd case *)
  16
  17 (** val void_rect_Type5 : void -> 'a1 **)
  18 let rec void_rect_Type5 x_328 =
  19   assert false (* absurd case *)
  20
  21 (** val void_rect_Type3 : void -> 'a1 **)
  22 let rec void_rect_Type3 x_329 =
  23   assert false (* absurd case *)
  24
  25 (** val void_rect_Type2 : void -> 'a1 **)
  26 let rec void_rect_Type2 x_330 =
  27   assert false (* absurd case *)
  28
  29 (** val void_rect_Type1 : void -> 'a1 **)
  30 let rec void_rect_Type1 x_331 =
  31   assert false (* absurd case *)
  32
  33 (** val void_rect_Type0 : void -> 'a1 **)
  34 let rec void_rect_Type0 x_332 =
  35   assert false (* absurd case *)
  36
  37 type unit0 =
  38 | It
  39
  40 (** val unit_rect_Type4 : 'a1 -> unit0 -> 'a1 **)
  41 let rec unit_rect_Type4 h_it = function
  42 | It -> h_it
  43
  44 (** val unit_rect_Type5 : 'a1 -> unit0 -> 'a1 **)
  45 let rec unit_rect_Type5 h_it = function
  46 | It -> h_it
  47
  48 (** val unit_rect_Type3 : 'a1 -> unit0 -> 'a1 **)
  49 let rec unit_rect_Type3 h_it = function
  50 | It -> h_it
  51
  52 (** val unit_rect_Type2 : 'a1 -> unit0 -> 'a1 **)
  53 let rec unit_rect_Type2 h_it = function
  54 | It -> h_it
  55
  56 (** val unit_rect_Type1 : 'a1 -> unit0 -> 'a1 **)
  57 let rec unit_rect_Type1 h_it = function
  58 | It -> h_it
  59
  60 (** val unit_rect_Type0 : 'a1 -> unit0 -> 'a1 **)
  61 let rec unit_rect_Type0 h_it = function
  62 | It -> h_it
  63
  64 (** val unit_inv_rect_Type4 : unit0 -> (__ -> 'a1) -> 'a1 **)
  65 let unit_inv_rect_Type4 hterm h1 =
  66   let hcut = unit_rect_Type4 h1 hterm in hcut __
  67
  68 (** val unit_inv_rect_Type3 : unit0 -> (__ -> 'a1) -> 'a1 **)
  69 let unit_inv_rect_Type3 hterm h1 =
  70   let hcut = unit_rect_Type3 h1 hterm in hcut __
  71
  72 (** val unit_inv_rect_Type2 : unit0 -> (__ -> 'a1) -> 'a1 **)
  73 let unit_inv_rect_Type2 hterm h1 =
  74   let hcut = unit_rect_Type2 h1 hterm in hcut __
  75
  76 (** val unit_inv_rect_Type1 : unit0 -> (__ -> 'a1) -> 'a1 **)
  77 let unit_inv_rect_Type1 hterm h1 =
  78   let hcut = unit_rect_Type1 h1 hterm in hcut __
  79
  80 (** val unit_inv_rect_Type0 : unit0 -> (__ -> 'a1) -> 'a1 **)
  81 let unit_inv_rect_Type0 hterm h1 =
  82   let hcut = unit_rect_Type0 h1 hterm in hcut __
  83
  84 (** val unit_discr : unit0 -> unit0 -> __ **)
  85 let unit_discr x y =
  86   Logic.eq_rect_Type2 x (let It = x in Obj.magic (fun _ dH -> dH)) y
  87
  88 type ('a, 'b) sum =
  89 | Inl of 'a
  90 | Inr of 'b
  91
  92 (** val sum_rect_Type4 :
  93     ('a1 -> 'a3) -> ('a2 -> 'a3) -> ('a1, 'a2) sum -> 'a3 **)
  94 let rec sum_rect_Type4 h_inl h_inr = function
  95 | Inl x_371 -> h_inl x_371
  96 | Inr x_372 -> h_inr x_372
  97
  98 (** val sum_rect_Type5 :
  99     ('a1 -> 'a3) -> ('a2 -> 'a3) -> ('a1, 'a2) sum -> 'a3 **)
 100 let rec sum_rect_Type5 h_inl h_inr = function
 101 | Inl x_376 -> h_inl x_376
 102 | Inr x_377 -> h_inr x_377
 103
 104 (** val sum_rect_Type3 :
 105     ('a1 -> 'a3) -> ('a2 -> 'a3) -> ('a1, 'a2) sum -> 'a3 **)
 106 let rec sum_rect_Type3 h_inl h_inr = function
 107 | Inl x_381 -> h_inl x_381
 108 | Inr x_382 -> h_inr x_382
 109
 110 (** val sum_rect_Type2 :
 111     ('a1 -> 'a3) -> ('a2 -> 'a3) -> ('a1, 'a2) sum -> 'a3 **)
 112 let rec sum_rect_Type2 h_inl h_inr = function
 113 | Inl x_386 -> h_inl x_386
 114 | Inr x_387 -> h_inr x_387
 115
 116 (** val sum_rect_Type1 :
 117     ('a1 -> 'a3) -> ('a2 -> 'a3) -> ('a1, 'a2) sum -> 'a3 **)
 118 let rec sum_rect_Type1 h_inl h_inr = function
 119 | Inl x_391 -> h_inl x_391
 120 | Inr x_392 -> h_inr x_392
 121
 122 (** val sum_rect_Type0 :
 123     ('a1 -> 'a3) -> ('a2 -> 'a3) -> ('a1, 'a2) sum -> 'a3 **)
 124 let rec sum_rect_Type0 h_inl h_inr = function
 125 | Inl x_396 -> h_inl x_396
 126 | Inr x_397 -> h_inr x_397
 127
 128 (** val sum_inv_rect_Type4 :
 129     ('a1, 'a2) sum -> ('a1 -> __ -> 'a3) -> ('a2 -> __ -> 'a3) -> 'a3 **)
 130 let sum_inv_rect_Type4 hterm h1 h2 =
 131   let hcut = sum_rect_Type4 h1 h2 hterm in hcut __
 132
 133 (** val sum_inv_rect_Type3 :
 134     ('a1, 'a2) sum -> ('a1 -> __ -> 'a3) -> ('a2 -> __ -> 'a3) -> 'a3 **)
 135 let sum_inv_rect_Type3 hterm h1 h2 =
 136   let hcut = sum_rect_Type3 h1 h2 hterm in hcut __
 137
 138 (** val sum_inv_rect_Type2 :
 139     ('a1, 'a2) sum -> ('a1 -> __ -> 'a3) -> ('a2 -> __ -> 'a3) -> 'a3 **)
 140 let sum_inv_rect_Type2 hterm h1 h2 =
 141   let hcut = sum_rect_Type2 h1 h2 hterm in hcut __
 142
 143 (** val sum_inv_rect_Type1 :
 144     ('a1, 'a2) sum -> ('a1 -> __ -> 'a3) -> ('a2 -> __ -> 'a3) -> 'a3 **)
 145 let sum_inv_rect_Type1 hterm h1 h2 =
 146   let hcut = sum_rect_Type1 h1 h2 hterm in hcut __
 147
 148 (** val sum_inv_rect_Type0 :
 149     ('a1, 'a2) sum -> ('a1 -> __ -> 'a3) -> ('a2 -> __ -> 'a3) -> 'a3 **)
 150 let sum_inv_rect_Type0 hterm h1 h2 =
 151   let hcut = sum_rect_Type0 h1 h2 hterm in hcut __
 152
 153 (** val sum_discr : ('a1, 'a2) sum -> ('a1, 'a2) sum -> __ **)
 154 let sum_discr x y =
 155   Logic.eq_rect_Type2 x
 156     (match x with
 157      | Inl a0 -> Obj.magic (fun _ dH -> dH __)
 158      | Inr a0 -> Obj.magic (fun _ dH -> dH __)) y
 159
 160 type 'a option =
 161 | None
 162 | Some of 'a
 163
 164 (** val option_rect_Type4 : 'a2 -> ('a1 -> 'a2) -> 'a1 option -> 'a2 **)
 165 let rec option_rect_Type4 h_None h_Some = function
 166 | None -> h_None
 167 | Some x_435 -> h_Some x_435
 168
 169 (** val option_rect_Type5 : 'a2 -> ('a1 -> 'a2) -> 'a1 option -> 'a2 **)
 170 let rec option_rect_Type5 h_None h_Some = function
 171 | None -> h_None
 172 | Some x_439 -> h_Some x_439
 173
 174 (** val option_rect_Type3 : 'a2 -> ('a1 -> 'a2) -> 'a1 option -> 'a2 **)
 175 let rec option_rect_Type3 h_None h_Some = function
 176 | None -> h_None
 177 | Some x_443 -> h_Some x_443
 178
 179 (** val option_rect_Type2 : 'a2 -> ('a1 -> 'a2) -> 'a1 option -> 'a2 **)
 180 let rec option_rect_Type2 h_None h_Some = function
 181 | None -> h_None
 182 | Some x_447 -> h_Some x_447
 183
 184 (** val option_rect_Type1 : 'a2 -> ('a1 -> 'a2) -> 'a1 option -> 'a2 **)
 185 let rec option_rect_Type1 h_None h_Some = function
 186 | None -> h_None
 187 | Some x_451 -> h_Some x_451
 188
 189 (** val option_rect_Type0 : 'a2 -> ('a1 -> 'a2) -> 'a1 option -> 'a2 **)
 190 let rec option_rect_Type0 h_None h_Some = function
 191 | None -> h_None
 192 | Some x_455 -> h_Some x_455
 193
 194 (** val option_inv_rect_Type4 :
 195     'a1 option -> (__ -> 'a2) -> ('a1 -> __ -> 'a2) -> 'a2 **)
 196 let option_inv_rect_Type4 hterm h1 h2 =
 197   let hcut = option_rect_Type4 h1 h2 hterm in hcut __
 198
 199 (** val option_inv_rect_Type3 :
 200     'a1 option -> (__ -> 'a2) -> ('a1 -> __ -> 'a2) -> 'a2 **)
 201 let option_inv_rect_Type3 hterm h1 h2 =
 202   let hcut = option_rect_Type3 h1 h2 hterm in hcut __
 203
 204 (** val option_inv_rect_Type2 :
 205     'a1 option -> (__ -> 'a2) -> ('a1 -> __ -> 'a2) -> 'a2 **)
 206 let option_inv_rect_Type2 hterm h1 h2 =
 207   let hcut = option_rect_Type2 h1 h2 hterm in hcut __
 208
 209 (** val option_inv_rect_Type1 :
 210     'a1 option -> (__ -> 'a2) -> ('a1 -> __ -> 'a2) -> 'a2 **)
 211 let option_inv_rect_Type1 hterm h1 h2 =
 212   let hcut = option_rect_Type1 h1 h2 hterm in hcut __
 213
 214 (** val option_inv_rect_Type0 :
 215     'a1 option -> (__ -> 'a2) -> ('a1 -> __ -> 'a2) -> 'a2 **)
 216 let option_inv_rect_Type0 hterm h1 h2 =
 217   let hcut = option_rect_Type0 h1 h2 hterm in hcut __
 218
 219 (** val option_discr : 'a1 option -> 'a1 option -> __ **)
 220 let option_discr x y =
 221   Logic.eq_rect_Type2 x
 222     (match x with
 223      | None -> Obj.magic (fun _ dH -> dH)
 224      | Some a0 -> Obj.magic (fun _ dH -> dH __)) y
 225
 226 (** val option_map : ('a1 -> 'a2) -> 'a1 option -> 'a2 option **)
 227 let option_map f = function
 228 | None -> None
 229 | Some a -> Some (f a)
 230
 231 (** val option_map_def : ('a1 -> 'a2) -> 'a2 -> 'a1 option -> 'a2 **)
 232 let option_map_def f d = function
 233 | None -> d
 234 | Some a -> f a
 235
 236 (** val refute_none_by_refl :
 237     ('a1 -> 'a2) -> 'a1 option -> ('a1 -> __ -> 'a3) -> 'a3 **)
 238 let refute_none_by_refl p clearme x =
 239   (match clearme with
 240    | None -> (fun _ -> assert false (* absurd case *))
 241    | Some a -> (fun _ p0 -> p0 a __)) __ x
 242
 243 type ('a, 'f) dPair = { dpi1 : 'a; dpi2 : 'f }
 244
 245 (** val dPair_rect_Type4 : ('a1 -> 'a2 -> 'a3) -> ('a1, 'a2) dPair -> 'a3 **)
 246 let rec dPair_rect_Type4 h_mk_DPair x_484 =
 247   let { dpi1 = dpi3; dpi2 = dpi4 } = x_484 in h_mk_DPair dpi3 dpi4
 248
 249 (** val dPair_rect_Type5 : ('a1 -> 'a2 -> 'a3) -> ('a1, 'a2) dPair -> 'a3 **)
 250 let rec dPair_rect_Type5 h_mk_DPair x_486 =
 251   let { dpi1 = dpi3; dpi2 = dpi4 } = x_486 in h_mk_DPair dpi3 dpi4
 252
 253 (** val dPair_rect_Type3 : ('a1 -> 'a2 -> 'a3) -> ('a1, 'a2) dPair -> 'a3 **)
 254 let rec dPair_rect_Type3 h_mk_DPair x_488 =
 255   let { dpi1 = dpi3; dpi2 = dpi4 } = x_488 in h_mk_DPair dpi3 dpi4
 256
 257 (** val dPair_rect_Type2 : ('a1 -> 'a2 -> 'a3) -> ('a1, 'a2) dPair -> 'a3 **)
 258 let rec dPair_rect_Type2 h_mk_DPair x_490 =
 259   let { dpi1 = dpi3; dpi2 = dpi4 } = x_490 in h_mk_DPair dpi3 dpi4
 260
 261 (** val dPair_rect_Type1 : ('a1 -> 'a2 -> 'a3) -> ('a1, 'a2) dPair -> 'a3 **)
 262 let rec dPair_rect_Type1 h_mk_DPair x_492 =
 263   let { dpi1 = dpi3; dpi2 = dpi4 } = x_492 in h_mk_DPair dpi3 dpi4
 264
 265 (** val dPair_rect_Type0 : ('a1 -> 'a2 -> 'a3) -> ('a1, 'a2) dPair -> 'a3 **)
 266 let rec dPair_rect_Type0 h_mk_DPair x_494 =
 267   let { dpi1 = dpi3; dpi2 = dpi4 } = x_494 in h_mk_DPair dpi3 dpi4
 268
 269 (** val dpi1 : ('a1, 'a2) dPair -> 'a1 **)
 270 let rec dpi1 xxx =
 271   xxx.dpi1
 272
 273 (** val dpi2 : ('a1, 'a2) dPair -> 'a2 **)
 274 let rec dpi2 xxx =
 275   xxx.dpi2
 276
 277 (** val dPair_inv_rect_Type4 :
 278     ('a1, 'a2) dPair -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3 **)
 279 let dPair_inv_rect_Type4 hterm h1 =
 280   let hcut = dPair_rect_Type4 h1 hterm in hcut __
 281
 282 (** val dPair_inv_rect_Type3 :
 283     ('a1, 'a2) dPair -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3 **)
 284 let dPair_inv_rect_Type3 hterm h1 =
 285   let hcut = dPair_rect_Type3 h1 hterm in hcut __
 286
 287 (** val dPair_inv_rect_Type2 :
 288     ('a1, 'a2) dPair -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3 **)
 289 let dPair_inv_rect_Type2 hterm h1 =
 290   let hcut = dPair_rect_Type2 h1 hterm in hcut __
 291
 292 (** val dPair_inv_rect_Type1 :
 293     ('a1, 'a2) dPair -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3 **)
 294 let dPair_inv_rect_Type1 hterm h1 =
 295   let hcut = dPair_rect_Type1 h1 hterm in hcut __
 296
 297 (** val dPair_inv_rect_Type0 :
 298     ('a1, 'a2) dPair -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3 **)
 299 let dPair_inv_rect_Type0 hterm h1 =
 300   let hcut = dPair_rect_Type0 h1 hterm in hcut __
 301
 302 (** val dPair_discr : ('a1, 'a2) dPair -> ('a1, 'a2) dPair -> __ **)
 303 let dPair_discr x y =
 304   Logic.eq_rect_Type2 x
 305     (let { dpi1 = a0; dpi2 = a10 } = x in Obj.magic (fun _ dH -> dH __ __)) y
 306
 307 type 'a sig0 =
 308   'a
 309   (* singleton inductive, whose constructor was mk_Sig *)
 310
 311 (** val sig_rect_Type4 : ('a1 -> __ -> 'a2) -> 'a1 sig0 -> 'a2 **)
 312 let rec sig_rect_Type4 h_mk_Sig x_510 =
 313   let pi1 = x_510 in h_mk_Sig pi1 __
 314
 315 (** val sig_rect_Type5 : ('a1 -> __ -> 'a2) -> 'a1 sig0 -> 'a2 **)
 316 let rec sig_rect_Type5 h_mk_Sig x_512 =
 317   let pi1 = x_512 in h_mk_Sig pi1 __
 318
 319 (** val sig_rect_Type3 : ('a1 -> __ -> 'a2) -> 'a1 sig0 -> 'a2 **)
 320 let rec sig_rect_Type3 h_mk_Sig x_514 =
 321   let pi1 = x_514 in h_mk_Sig pi1 __
 322
 323 (** val sig_rect_Type2 : ('a1 -> __ -> 'a2) -> 'a1 sig0 -> 'a2 **)
 324 let rec sig_rect_Type2 h_mk_Sig x_516 =
 325   let pi1 = x_516 in h_mk_Sig pi1 __
 326
 327 (** val sig_rect_Type1 : ('a1 -> __ -> 'a2) -> 'a1 sig0 -> 'a2 **)
 328 let rec sig_rect_Type1 h_mk_Sig x_518 =
 329   let pi1 = x_518 in h_mk_Sig pi1 __
 330
 331 (** val sig_rect_Type0 : ('a1 -> __ -> 'a2) -> 'a1 sig0 -> 'a2 **)
 332 let rec sig_rect_Type0 h_mk_Sig x_520 =
 333   let pi1 = x_520 in h_mk_Sig pi1 __
 334
 335 (** val pi1 : 'a1 sig0 -> 'a1 **)
 336 let rec pi1 xxx =
 337   let yyy = xxx in yyy
 338
 339 (** val sig_inv_rect_Type4 : 'a1 sig0 -> ('a1 -> __ -> __ -> 'a2) -> 'a2 **)
 340 let sig_inv_rect_Type4 hterm h1 =
 341   let hcut = sig_rect_Type4 h1 hterm in hcut __
 342
 343 (** val sig_inv_rect_Type3 : 'a1 sig0 -> ('a1 -> __ -> __ -> 'a2) -> 'a2 **)
 344 let sig_inv_rect_Type3 hterm h1 =
 345   let hcut = sig_rect_Type3 h1 hterm in hcut __
 346
 347 (** val sig_inv_rect_Type2 : 'a1 sig0 -> ('a1 -> __ -> __ -> 'a2) -> 'a2 **)
 348 let sig_inv_rect_Type2 hterm h1 =
 349   let hcut = sig_rect_Type2 h1 hterm in hcut __
 350
 351 (** val sig_inv_rect_Type1 : 'a1 sig0 -> ('a1 -> __ -> __ -> 'a2) -> 'a2 **)
 352 let sig_inv_rect_Type1 hterm h1 =
 353   let hcut = sig_rect_Type1 h1 hterm in hcut __
 354
 355 (** val sig_inv_rect_Type0 : 'a1 sig0 -> ('a1 -> __ -> __ -> 'a2) -> 'a2 **)
 356 let sig_inv_rect_Type0 hterm h1 =
 357   let hcut = sig_rect_Type0 h1 hterm in hcut __
 358
 359 (** val sig_discr : 'a1 sig0 -> 'a1 sig0 -> __ **)
 360 let sig_discr x y =
 361   Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __ __)) y
 362
 363 type ('a, 'b) prod = { fst : 'a; snd : 'b }
 364
 365 (** val prod_rect_Type4 : ('a1 -> 'a2 -> 'a3) -> ('a1, 'a2) prod -> 'a3 **)
 366 let rec prod_rect_Type4 h_mk_Prod x_536 =
 367   let { fst = fst0; snd = snd0 } = x_536 in h_mk_Prod fst0 snd0
 368
 369 (** val prod_rect_Type5 : ('a1 -> 'a2 -> 'a3) -> ('a1, 'a2) prod -> 'a3 **)
 370 let rec prod_rect_Type5 h_mk_Prod x_538 =
 371   let { fst = fst0; snd = snd0 } = x_538 in h_mk_Prod fst0 snd0
 372
 373 (** val prod_rect_Type3 : ('a1 -> 'a2 -> 'a3) -> ('a1, 'a2) prod -> 'a3 **)
 374 let rec prod_rect_Type3 h_mk_Prod x_540 =
 375   let { fst = fst0; snd = snd0 } = x_540 in h_mk_Prod fst0 snd0
 376
 377 (** val prod_rect_Type2 : ('a1 -> 'a2 -> 'a3) -> ('a1, 'a2) prod -> 'a3 **)
 378 let rec prod_rect_Type2 h_mk_Prod x_542 =
 379   let { fst = fst0; snd = snd0 } = x_542 in h_mk_Prod fst0 snd0
 380
 381 (** val prod_rect_Type1 : ('a1 -> 'a2 -> 'a3) -> ('a1, 'a2) prod -> 'a3 **)
 382 let rec prod_rect_Type1 h_mk_Prod x_544 =
 383   let { fst = fst0; snd = snd0 } = x_544 in h_mk_Prod fst0 snd0
 384
 385 (** val prod_rect_Type0 : ('a1 -> 'a2 -> 'a3) -> ('a1, 'a2) prod -> 'a3 **)
 386 let rec prod_rect_Type0 h_mk_Prod x_546 =
 387   let { fst = fst0; snd = snd0 } = x_546 in h_mk_Prod fst0 snd0
 388
 389 (** val fst : ('a1, 'a2) prod -> 'a1 **)
 390 let rec fst xxx =
 391   xxx.fst
 392
 393 (** val snd : ('a1, 'a2) prod -> 'a2 **)
 394 let rec snd xxx =
 395   xxx.snd
 396
 397 (** val prod_inv_rect_Type4 :
 398     ('a1, 'a2) prod -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3 **)
 399 let prod_inv_rect_Type4 hterm h1 =
 400   let hcut = prod_rect_Type4 h1 hterm in hcut __
 401
 402 (** val prod_inv_rect_Type3 :
 403     ('a1, 'a2) prod -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3 **)
 404 let prod_inv_rect_Type3 hterm h1 =
 405   let hcut = prod_rect_Type3 h1 hterm in hcut __
 406
 407 (** val prod_inv_rect_Type2 :
 408     ('a1, 'a2) prod -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3 **)
 409 let prod_inv_rect_Type2 hterm h1 =
 410   let hcut = prod_rect_Type2 h1 hterm in hcut __
 411
 412 (** val prod_inv_rect_Type1 :
 413     ('a1, 'a2) prod -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3 **)
 414 let prod_inv_rect_Type1 hterm h1 =
 415   let hcut = prod_rect_Type1 h1 hterm in hcut __
 416
 417 (** val prod_inv_rect_Type0 :
 418     ('a1, 'a2) prod -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3 **)
 419 let prod_inv_rect_Type0 hterm h1 =
 420   let hcut = prod_rect_Type0 h1 hterm in hcut __
 421
 422 (** val prod_discr : ('a1, 'a2) prod -> ('a1, 'a2) prod -> __ **)
 423 let prod_discr x y =
 424   Logic.eq_rect_Type2 x
 425     (let { fst = a0; snd = a10 } = x in Obj.magic (fun _ dH -> dH __ __)) y
 426
 427 (** val coerc_pair_sigma : ('a1, 'a2) prod -> ('a1, 'a2 sig0) prod **)
 428 let coerc_pair_sigma clearme =
 429   (let { fst = a; snd = b } = clearme in (fun _ -> { fst = a; snd = b })) __
 430
 431 (** val dpi1__o__coerc_pair_sigma :
 432     (('a1, 'a2) prod, 'a3) dPair -> ('a1, 'a2 sig0) prod **)
 433 let dpi1__o__coerc_pair_sigma x4 =
 434   coerc_pair_sigma x4.dpi1
 435