open Preamble

open Hints_declaration

open Core_notation

open Pts

open Logic

type sigma =
  __
  (* singleton inductive, whose constructor was mk_Sigma *)

val sigma_rect_Type4 : (__ -> __ -> 'a1) -> sigma -> 'a1

val sigma_rect_Type5 : (__ -> __ -> 'a1) -> sigma -> 'a1

val sigma_rect_Type3 : (__ -> __ -> 'a1) -> sigma -> 'a1

val sigma_rect_Type2 : (__ -> __ -> 'a1) -> sigma -> 'a1

val sigma_rect_Type1 : (__ -> __ -> 'a1) -> sigma -> 'a1

val sigma_rect_Type0 : (__ -> __ -> 'a1) -> sigma -> 'a1

val sigma_inv_rect_Type4 : sigma -> (__ -> __ -> __ -> 'a1) -> 'a1

val sigma_inv_rect_Type3 : sigma -> (__ -> __ -> __ -> 'a1) -> 'a1

val sigma_inv_rect_Type2 : sigma -> (__ -> __ -> __ -> 'a1) -> 'a1

val sigma_inv_rect_Type1 : sigma -> (__ -> __ -> __ -> 'a1) -> 'a1

val sigma_inv_rect_Type0 : sigma -> (__ -> __ -> __ -> 'a1) -> 'a1

type p1 = __

val p2 : sigma -> p1

val jmeq_rect_Type4 : 'a1 -> 'a2 -> 'a3 -> 'a2

val jmeq_rect_Type5 : 'a1 -> 'a2 -> 'a3 -> 'a2

val jmeq_rect_Type3 : 'a1 -> 'a2 -> 'a3 -> 'a2

val jmeq_rect_Type2 : 'a1 -> 'a2 -> 'a3 -> 'a2

val jmeq_rect_Type1 : 'a1 -> 'a2 -> 'a3 -> 'a2

val jmeq_rect_Type0 : 'a1 -> 'a2 -> 'a3 -> 'a2

val jmeq_inv_rect_Type4 : 'a1 -> 'a2 -> (__ -> __ -> 'a3) -> 'a3

val jmeq_inv_rect_Type3 : 'a1 -> 'a2 -> (__ -> __ -> 'a3) -> 'a3

val jmeq_inv_rect_Type2 : 'a1 -> 'a2 -> (__ -> __ -> 'a3) -> 'a3

val jmeq_inv_rect_Type1 : 'a1 -> 'a2 -> (__ -> __ -> 'a3) -> 'a3

val jmeq_inv_rect_Type0 : 'a1 -> 'a2 -> (__ -> __ -> 'a3) -> 'a3

val jmeq_discr : 'a1 -> 'a2 -> __

val cast : 'a1 -> 'a2

type ('a, 'x) curry = 'x

val g : 'a1 -> 'a2 -> 'a1 -> 'a2

type 'p pP = 'p

val e : 'a1 -> 'a2 pP -> 'a1 -> 'a2 pP

val jmeq_elim : 'a1 -> 'a2 -> 'a1 -> 'a2