source: extracted/jmeq.ml @ 2746

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_890 =
  let x_891 = x_890 in h_mk_Sigma __ x_891

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

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

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

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

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

(** 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_929 =
  h_refl_jmeq

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

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

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

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

(** val jmeq_rect_Type0 : 'a1 -> 'a2 -> 'a3 -> 'a2 **)
let rec jmeq_rect_Type0 x h_refl_jmeq x_944 =
  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