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 **)
let rec sigma_rect_Type4 h_mk_Sigma x_812 =
  let x_813 = x_812 in h_mk_Sigma __ x_813

(** val sigma_rect_Type5 : (__ -> __ -> 'a1) -> sigma -> 'a1 **)
let rec sigma_rect_Type5 h_mk_Sigma x_815 =
  let x_816 = x_815 in h_mk_Sigma __ x_816

(** val sigma_rect_Type3 : (__ -> __ -> 'a1) -> sigma -> 'a1 **)
let rec sigma_rect_Type3 h_mk_Sigma x_818 =
  let x_819 = x_818 in h_mk_Sigma __ x_819

(** val sigma_rect_Type2 : (__ -> __ -> 'a1) -> sigma -> 'a1 **)
let rec sigma_rect_Type2 h_mk_Sigma x_821 =
  let x_822 = x_821 in h_mk_Sigma __ x_822

(** val sigma_rect_Type1 : (__ -> __ -> 'a1) -> sigma -> 'a1 **)
let rec sigma_rect_Type1 h_mk_Sigma x_824 =
  let x_825 = x_824 in h_mk_Sigma __ x_825

(** val sigma_rect_Type0 : (__ -> __ -> 'a1) -> sigma -> 'a1 **)
let rec sigma_rect_Type0 h_mk_Sigma x_827 =
  let x_828 = x_827 in h_mk_Sigma __ x_828

(** val sigma_inv_rect_Type4 : sigma -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
let sigma_inv_rect_Type4 hterm h1 =
  let hcut = sigma_rect_Type4 h1 hterm in hcut __

(** val sigma_inv_rect_Type3 : sigma -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
let sigma_inv_rect_Type3 hterm h1 =
  let hcut = sigma_rect_Type3 h1 hterm in hcut __

(** val sigma_inv_rect_Type2 : sigma -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
let sigma_inv_rect_Type2 hterm h1 =
  let hcut = sigma_rect_Type2 h1 hterm in hcut __

(** val sigma_inv_rect_Type1 : sigma -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
let sigma_inv_rect_Type1 hterm h1 =
  let hcut = sigma_rect_Type1 h1 hterm in hcut __

(** val sigma_inv_rect_Type0 : sigma -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
let sigma_inv_rect_Type0 hterm h1 =
  let hcut = sigma_rect_Type0 h1 hterm in hcut __

type p1 = __

(** val p2 : sigma -> p1 **)
let p2 s =
  let x = s in x

(** val jmeq_rect_Type4 : 'a1 -> 'a2 -> 'a3 -> 'a2 **)
let rec jmeq_rect_Type4 x h_refl_jmeq x_851 =
  h_refl_jmeq

(** val jmeq_rect_Type5 : 'a1 -> 'a2 -> 'a3 -> 'a2 **)
let rec jmeq_rect_Type5 x h_refl_jmeq x_854 =
  h_refl_jmeq

(** val jmeq_rect_Type3 : 'a1 -> 'a2 -> 'a3 -> 'a2 **)
let rec jmeq_rect_Type3 x h_refl_jmeq x_857 =
  h_refl_jmeq

(** val jmeq_rect_Type2 : 'a1 -> 'a2 -> 'a3 -> 'a2 **)
let rec jmeq_rect_Type2 x h_refl_jmeq x_860 =
  h_refl_jmeq

(** val jmeq_rect_Type1 : 'a1 -> 'a2 -> 'a3 -> 'a2 **)
let rec jmeq_rect_Type1 x h_refl_jmeq x_863 =
  h_refl_jmeq

(** val jmeq_rect_Type0 : 'a1 -> 'a2 -> 'a3 -> 'a2 **)
let rec jmeq_rect_Type0 x h_refl_jmeq x_866 =
  h_refl_jmeq

(** val jmeq_inv_rect_Type4 : 'a1 -> 'a2 -> (__ -> __ -> 'a3) -> 'a3 **)
let jmeq_inv_rect_Type4 x2 x4 h1 =
  let hcut = jmeq_rect_Type4 x2 h1 x4 in hcut __ __

(** val jmeq_inv_rect_Type3 : 'a1 -> 'a2 -> (__ -> __ -> 'a3) -> 'a3 **)
let jmeq_inv_rect_Type3 x2 x4 h1 =
  let hcut = jmeq_rect_Type3 x2 h1 x4 in hcut __ __

(** val jmeq_inv_rect_Type2 : 'a1 -> 'a2 -> (__ -> __ -> 'a3) -> 'a3 **)
let jmeq_inv_rect_Type2 x2 x4 h1 =
  let hcut = jmeq_rect_Type2 x2 h1 x4 in hcut __ __

(** val jmeq_inv_rect_Type1 : 'a1 -> 'a2 -> (__ -> __ -> 'a3) -> 'a3 **)
let jmeq_inv_rect_Type1 x2 x4 h1 =
  let hcut = jmeq_rect_Type1 x2 h1 x4 in hcut __ __

(** val jmeq_inv_rect_Type0 : 'a1 -> 'a2 -> (__ -> __ -> 'a3) -> 'a3 **)
let jmeq_inv_rect_Type0 x2 x4 h1 =
  let hcut = jmeq_rect_Type0 x2 h1 x4 in hcut __ __

(** val jmeq_discr : 'a1 -> 'a2 -> __ **)
let jmeq_discr a2 a4 =
  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH)) __

(** val cast : 'a1 -> 'a2 **)
let cast x =
  (fun x0 -> Obj.magic x0) x

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

(** val g : 'a1 -> 'a2 -> 'a1 -> 'a2 **)
let g x h y =
  (fun _ -> Logic.eq_rect_Type0 __ h __) __

type 'p pP = 'p

(** val e : 'a1 -> 'a2 pP -> 'a1 -> 'a2 pP **)
let e a h b =
  let x = g a h b in x

(** val jmeq_elim : 'a1 -> 'a2 -> 'a1 -> 'a2 **)
let jmeq_elim x x0 y =
  e x x0 y