extracted/jmeq.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 sigma =
  12   __
  13   (* singleton inductive, whose constructor was mk_Sigma *)
  14
  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
  18
  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
  22
  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
  26
  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
  30
  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
  34
  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
  38
  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 __
  42
  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 __
  46
  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 __
  50
  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 __
  54
  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 __
  58
  59 type p1 = __
  60
  61 (** val p2 : sigma -> p1 **)
  62 let p2 s =
  63   let x = s in x
  64
  65 (** val jmeq_rect_Type4 : 'a1 -> 'a2 -> 'a3 -> 'a2 **)
  66 let rec jmeq_rect_Type4 x h_refl_jmeq x_851 =
  67   h_refl_jmeq
  68
  69 (** val jmeq_rect_Type5 : 'a1 -> 'a2 -> 'a3 -> 'a2 **)
  70 let rec jmeq_rect_Type5 x h_refl_jmeq x_854 =
  71   h_refl_jmeq
  72
  73 (** val jmeq_rect_Type3 : 'a1 -> 'a2 -> 'a3 -> 'a2 **)
  74 let rec jmeq_rect_Type3 x h_refl_jmeq x_857 =
  75   h_refl_jmeq
  76
  77 (** val jmeq_rect_Type2 : 'a1 -> 'a2 -> 'a3 -> 'a2 **)
  78 let rec jmeq_rect_Type2 x h_refl_jmeq x_860 =
  79   h_refl_jmeq
  80
  81 (** val jmeq_rect_Type1 : 'a1 -> 'a2 -> 'a3 -> 'a2 **)
  82 let rec jmeq_rect_Type1 x h_refl_jmeq x_863 =
  83   h_refl_jmeq
  84
  85 (** val jmeq_rect_Type0 : 'a1 -> 'a2 -> 'a3 -> 'a2 **)
  86 let rec jmeq_rect_Type0 x h_refl_jmeq x_866 =
  87   h_refl_jmeq
  88
  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 __ __
  92
  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 __ __
  96
  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 __ __
 100
 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 __ __
 104
 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 __ __
 108
 109 (** val jmeq_discr : 'a1 -> 'a2 -> __ **)
 110 let jmeq_discr a2 a4 =
 111   Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH)) __
 112
 113 (** val cast : 'a1 -> 'a2 **)
 114 let cast x =
 115   (fun x0 -> Obj.magic x0) x
 116
 117 type ('a, 'x) curry = 'x
 118
 119 (** val g : 'a1 -> 'a2 -> 'a1 -> 'a2 **)
 120 let g x h y =
 121   (fun _ -> Logic.eq_rect_Type0 __ h __) __
 122
 123 type 'p pP = 'p
 124
 125 (** val e : 'a1 -> 'a2 pP -> 'a1 -> 'a2 pP **)
 126 let e a h b =
 127   let x = g a h b in x
 128
 129 (** val jmeq_elim : 'a1 -> 'a2 -> 'a1 -> 'a2 **)
 130 let jmeq_elim x x0 y =
 131   e x x0 y
 132