extracted/logic.ml

   1 open Preamble
   2
   3 open Core_notation
   4
   5 open Pts
   6
   7 open Hints_declaration
   8
   9 (** val eq_rect_Type4 : 'a1 -> 'a2 -> 'a1 -> 'a2 **)
  10 let rec eq_rect_Type4 x h_refl x_4 =
  11   h_refl
  12
  13 (** val eq_rect_Type5 : 'a1 -> 'a2 -> 'a1 -> 'a2 **)
  14 let rec eq_rect_Type5 x h_refl x_7 =
  15   h_refl
  16
  17 (** val eq_rect_Type3 : 'a1 -> 'a2 -> 'a1 -> 'a2 **)
  18 let rec eq_rect_Type3 x h_refl x_10 =
  19   h_refl
  20
  21 (** val eq_rect_Type2 : 'a1 -> 'a2 -> 'a1 -> 'a2 **)
  22 let rec eq_rect_Type2 x h_refl x_13 =
  23   h_refl
  24
  25 (** val eq_rect_Type1 : 'a1 -> 'a2 -> 'a1 -> 'a2 **)
  26 let rec eq_rect_Type1 x h_refl x_16 =
  27   h_refl
  28
  29 (** val eq_rect_Type0 : 'a1 -> 'a2 -> 'a1 -> 'a2 **)
  30 let rec eq_rect_Type0 x h_refl x_19 =
  31   h_refl
  32
  33 (** val eq_rect_r : 'a1 -> 'a1 -> 'a2 -> 'a2 **)
  34 let eq_rect_r a x x0 =
  35   (fun _ auto -> auto) __ x0
  36
  37 (** val eq_rect_Type0_r : 'a1 -> 'a2 -> 'a1 -> 'a2 **)
  38 let eq_rect_Type0_r a h x =
  39   (fun _ auto -> auto) __ h
  40
  41 (** val eq_rect_Type1_r : 'a1 -> 'a2 -> 'a1 -> 'a2 **)
  42 let eq_rect_Type1_r a h x =
  43   (fun _ auto -> auto) __ h
  44
  45 (** val eq_rect_Type2_r : 'a1 -> 'a2 -> 'a1 -> 'a2 **)
  46 let eq_rect_Type2_r a h x =
  47   (fun _ auto -> auto) __ h
  48
  49 (** val eq_rect_Type3_r : 'a1 -> 'a2 -> 'a1 -> 'a2 **)
  50 let eq_rect_Type3_r a h x =
  51   (fun _ auto -> auto) __ h
  52
  53 (** val rewrite_l : 'a1 -> 'a2 -> 'a1 -> 'a2 **)
  54 let rewrite_l x hx y =
  55   hx
  56
  57 (** val rewrite_r : 'a1 -> 'a2 -> 'a1 -> 'a2 **)
  58 let rewrite_r x hx y =
  59   hx
  60
  61 (** val eq_coerc : 'a1 -> 'a2 **)
  62 let eq_coerc ha =
  63   eq_rect_Type0 __ (Obj.magic ha) __
  64
  65 (** val true_rect_Type4 : 'a1 -> 'a1 **)
  66 let rec true_rect_Type4 h_I =
  67   h_I
  68
  69 (** val true_rect_Type5 : 'a1 -> 'a1 **)
  70 let rec true_rect_Type5 h_I =
  71   h_I
  72
  73 (** val true_rect_Type3 : 'a1 -> 'a1 **)
  74 let rec true_rect_Type3 h_I =
  75   h_I
  76
  77 (** val true_rect_Type2 : 'a1 -> 'a1 **)
  78 let rec true_rect_Type2 h_I =
  79   h_I
  80
  81 (** val true_rect_Type1 : 'a1 -> 'a1 **)
  82 let rec true_rect_Type1 h_I =
  83   h_I
  84
  85 (** val true_rect_Type0 : 'a1 -> 'a1 **)
  86 let rec true_rect_Type0 h_I =
  87   h_I
  88
  89 (** val true_inv_rect_Type4 : (__ -> 'a1) -> 'a1 **)
  90 let true_inv_rect_Type4 h1 =
  91   let hcut = true_rect_Type4 h1 in hcut __
  92
  93 (** val true_inv_rect_Type3 : (__ -> 'a1) -> 'a1 **)
  94 let true_inv_rect_Type3 h1 =
  95   let hcut = true_rect_Type3 h1 in hcut __
  96
  97 (** val true_inv_rect_Type2 : (__ -> 'a1) -> 'a1 **)
  98 let true_inv_rect_Type2 h1 =
  99   let hcut = true_rect_Type2 h1 in hcut __
 100
 101 (** val true_inv_rect_Type1 : (__ -> 'a1) -> 'a1 **)
 102 let true_inv_rect_Type1 h1 =
 103   let hcut = true_rect_Type1 h1 in hcut __
 104
 105 (** val true_inv_rect_Type0 : (__ -> 'a1) -> 'a1 **)
 106 let true_inv_rect_Type0 h1 =
 107   let hcut = true_rect_Type0 h1 in hcut __
 108
 109 (** val true_discr : __ -> __ **)
 110 let true_discr _ =
 111   eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH)) __
 112
 113 (** val false_rect_Type4 : __ -> 'a1 **)
 114 let rec false_rect_Type4 _ =
 115   assert false (* absurd case *)
 116
 117 (** val false_rect_Type5 : __ -> 'a1 **)
 118 let rec false_rect_Type5 _ =
 119   assert false (* absurd case *)
 120
 121 (** val false_rect_Type3 : __ -> 'a1 **)
 122 let rec false_rect_Type3 _ =
 123   assert false (* absurd case *)
 124
 125 (** val false_rect_Type2 : __ -> 'a1 **)
 126 let rec false_rect_Type2 _ =
 127   assert false (* absurd case *)
 128
 129 (** val false_rect_Type1 : __ -> 'a1 **)
 130 let rec false_rect_Type1 _ =
 131   assert false (* absurd case *)
 132
 133 (** val false_rect_Type0 : __ -> 'a1 **)
 134 let rec false_rect_Type0 _ =
 135   assert false (* absurd case *)
 136
 137 (** val not_rect_Type4 : (__ -> 'a1) -> 'a1 **)
 138 let rec not_rect_Type4 h_nmk =
 139   h_nmk __
 140
 141 (** val not_rect_Type5 : (__ -> 'a1) -> 'a1 **)
 142 let rec not_rect_Type5 h_nmk =
 143   h_nmk __
 144
 145 (** val not_rect_Type3 : (__ -> 'a1) -> 'a1 **)
 146 let rec not_rect_Type3 h_nmk =
 147   h_nmk __
 148
 149 (** val not_rect_Type2 : (__ -> 'a1) -> 'a1 **)
 150 let rec not_rect_Type2 h_nmk =
 151   h_nmk __
 152
 153 (** val not_rect_Type1 : (__ -> 'a1) -> 'a1 **)
 154 let rec not_rect_Type1 h_nmk =
 155   h_nmk __
 156
 157 (** val not_rect_Type0 : (__ -> 'a1) -> 'a1 **)
 158 let rec not_rect_Type0 h_nmk =
 159   h_nmk __
 160
 161 (** val not_inv_rect_Type4 : (__ -> __ -> 'a1) -> 'a1 **)
 162 let not_inv_rect_Type4 h1 =
 163   let hcut = not_rect_Type4 h1 in hcut __
 164
 165 (** val not_inv_rect_Type3 : (__ -> __ -> 'a1) -> 'a1 **)
 166 let not_inv_rect_Type3 h1 =
 167   let hcut = not_rect_Type3 h1 in hcut __
 168
 169 (** val not_inv_rect_Type2 : (__ -> __ -> 'a1) -> 'a1 **)
 170 let not_inv_rect_Type2 h1 =
 171   let hcut = not_rect_Type2 h1 in hcut __
 172
 173 (** val not_inv_rect_Type1 : (__ -> __ -> 'a1) -> 'a1 **)
 174 let not_inv_rect_Type1 h1 =
 175   let hcut = not_rect_Type1 h1 in hcut __
 176
 177 (** val not_inv_rect_Type0 : (__ -> __ -> 'a1) -> 'a1 **)
 178 let not_inv_rect_Type0 h1 =
 179   let hcut = not_rect_Type0 h1 in hcut __
 180
 181 (** val and_rect_Type4 : (__ -> __ -> 'a1) -> 'a1 **)
 182 let rec and_rect_Type4 h_conj =
 183   h_conj __ __
 184
 185 (** val and_rect_Type5 : (__ -> __ -> 'a1) -> 'a1 **)
 186 let rec and_rect_Type5 h_conj =
 187   h_conj __ __
 188
 189 (** val and_rect_Type3 : (__ -> __ -> 'a1) -> 'a1 **)
 190 let rec and_rect_Type3 h_conj =
 191   h_conj __ __
 192
 193 (** val and_rect_Type2 : (__ -> __ -> 'a1) -> 'a1 **)
 194 let rec and_rect_Type2 h_conj =
 195   h_conj __ __
 196
 197 (** val and_rect_Type1 : (__ -> __ -> 'a1) -> 'a1 **)
 198 let rec and_rect_Type1 h_conj =
 199   h_conj __ __
 200
 201 (** val and_rect_Type0 : (__ -> __ -> 'a1) -> 'a1 **)
 202 let rec and_rect_Type0 h_conj =
 203   h_conj __ __
 204
 205 (** val and_inv_rect_Type4 : (__ -> __ -> __ -> 'a1) -> 'a1 **)
 206 let and_inv_rect_Type4 h1 =
 207   let hcut = and_rect_Type4 h1 in hcut __
 208
 209 (** val and_inv_rect_Type3 : (__ -> __ -> __ -> 'a1) -> 'a1 **)
 210 let and_inv_rect_Type3 h1 =
 211   let hcut = and_rect_Type3 h1 in hcut __
 212
 213 (** val and_inv_rect_Type2 : (__ -> __ -> __ -> 'a1) -> 'a1 **)
 214 let and_inv_rect_Type2 h1 =
 215   let hcut = and_rect_Type2 h1 in hcut __
 216
 217 (** val and_inv_rect_Type1 : (__ -> __ -> __ -> 'a1) -> 'a1 **)
 218 let and_inv_rect_Type1 h1 =
 219   let hcut = and_rect_Type1 h1 in hcut __
 220
 221 (** val and_inv_rect_Type0 : (__ -> __ -> __ -> 'a1) -> 'a1 **)
 222 let and_inv_rect_Type0 h1 =
 223   let hcut = and_rect_Type0 h1 in hcut __
 224
 225 (** val r0 : 'a1 -> 'a1 **)
 226 let r0 t =
 227   t
 228
 229 (** val r1 : 'a1 -> 'a2 -> 'a1 -> 'a2 **)
 230 let r1 x h_refl x_19 =
 231   eq_rect_Type0 x h_refl x_19
 232
 233 (** val r2 : 'a1 -> 'a2 -> 'a3 -> 'a1 -> 'a2 -> 'a3 **)
 234 let r2 a0 a1 a2 b0 b1 =
 235   eq_rect_Type0 (r1 a0 a1 b0) (r1 a0 a2 b0) b1
 236
 237 (** val r3 : 'a1 -> 'a2 -> 'a3 -> 'a4 -> 'a1 -> 'a2 -> 'a3 -> 'a4 **)
 238 let r3 a0 a1 a2 a3 b0 b1 b2 =
 239   eq_rect_Type0 (r2 a0 a1 a2 b0 b1) (r2 a0 a1 a3 b0 b1) b2
 240
 241 (** val r4 :
 242     'a1 -> 'a2 -> 'a3 -> 'a4 -> 'a5 -> 'a1 -> 'a2 -> 'a3 -> 'a4 -> 'a5 **)
 243 let r4 a0 a1 a2 a3 a4 b0 b1 b2 b3 =
 244   eq_rect_Type0 (r3 a0 a1 a2 a3 b0 b1 b2) (r3 a0 a1 a2 a4 b0 b1 b2) b3
 245
 246 (** val streicherK : 'a1 -> 'a2 -> 'a2 **)
 247 let streicherK t h =
 248   eq_rect_Type3_r __ h __
 249