source: extracted/logic.ml @ 2746

open Preamble

open Core_notation

open Pts

open Hints_declaration

(** val eq_rect_Type4 : 'a1 -> 'a2 -> 'a1 -> 'a2 **)
let rec eq_rect_Type4 x h_refl x_4 =
  h_refl

(** val eq_rect_Type5 : 'a1 -> 'a2 -> 'a1 -> 'a2 **)
let rec eq_rect_Type5 x h_refl x_7 =
  h_refl

(** val eq_rect_Type3 : 'a1 -> 'a2 -> 'a1 -> 'a2 **)
let rec eq_rect_Type3 x h_refl x_10 =
  h_refl

(** val eq_rect_Type2 : 'a1 -> 'a2 -> 'a1 -> 'a2 **)
let rec eq_rect_Type2 x h_refl x_13 =
  h_refl

(** val eq_rect_Type1 : 'a1 -> 'a2 -> 'a1 -> 'a2 **)
let rec eq_rect_Type1 x h_refl x_16 =
  h_refl

(** val eq_rect_Type0 : 'a1 -> 'a2 -> 'a1 -> 'a2 **)
let rec eq_rect_Type0 x h_refl x_19 =
  h_refl

(** val eq_rect_r : 'a1 -> 'a1 -> 'a2 -> 'a2 **)
let eq_rect_r a x x0 =
  (fun _ auto -> auto) __ x0

(** val eq_rect_Type0_r : 'a1 -> 'a2 -> 'a1 -> 'a2 **)
let eq_rect_Type0_r a h x =
  (fun _ auto -> auto) __ h

(** val eq_rect_Type1_r : 'a1 -> 'a2 -> 'a1 -> 'a2 **)
let eq_rect_Type1_r a h x =
  (fun _ auto -> auto) __ h

(** val eq_rect_Type2_r : 'a1 -> 'a2 -> 'a1 -> 'a2 **)
let eq_rect_Type2_r a h x =
  (fun _ auto -> auto) __ h

(** val eq_rect_Type3_r : 'a1 -> 'a2 -> 'a1 -> 'a2 **)
let eq_rect_Type3_r a h x =
  (fun _ auto -> auto) __ h

(** val rewrite_l : 'a1 -> 'a2 -> 'a1 -> 'a2 **)
let rewrite_l x hx y =
  hx

(** val rewrite_r : 'a1 -> 'a2 -> 'a1 -> 'a2 **)
let rewrite_r x hx y =
  hx

(** val eq_coerc : 'a1 -> 'a2 **)
let eq_coerc ha =
  eq_rect_Type0 __ (Obj.magic ha) __

(** val true_rect_Type4 : 'a1 -> 'a1 **)
let rec true_rect_Type4 h_I =
  h_I

(** val true_rect_Type5 : 'a1 -> 'a1 **)
let rec true_rect_Type5 h_I =
  h_I

(** val true_rect_Type3 : 'a1 -> 'a1 **)
let rec true_rect_Type3 h_I =
  h_I

(** val true_rect_Type2 : 'a1 -> 'a1 **)
let rec true_rect_Type2 h_I =
  h_I

(** val true_rect_Type1 : 'a1 -> 'a1 **)
let rec true_rect_Type1 h_I =
  h_I

(** val true_rect_Type0 : 'a1 -> 'a1 **)
let rec true_rect_Type0 h_I =
  h_I

(** val true_inv_rect_Type4 : (__ -> 'a1) -> 'a1 **)
let true_inv_rect_Type4 h1 =
  let hcut = true_rect_Type4 h1 in hcut __

(** val true_inv_rect_Type3 : (__ -> 'a1) -> 'a1 **)
let true_inv_rect_Type3 h1 =
  let hcut = true_rect_Type3 h1 in hcut __

(** val true_inv_rect_Type2 : (__ -> 'a1) -> 'a1 **)
let true_inv_rect_Type2 h1 =
  let hcut = true_rect_Type2 h1 in hcut __

(** val true_inv_rect_Type1 : (__ -> 'a1) -> 'a1 **)
let true_inv_rect_Type1 h1 =
  let hcut = true_rect_Type1 h1 in hcut __

(** val true_inv_rect_Type0 : (__ -> 'a1) -> 'a1 **)
let true_inv_rect_Type0 h1 =
  let hcut = true_rect_Type0 h1 in hcut __

(** val true_discr : __ -> __ **)
let true_discr _ =
  eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH)) __

(** val false_rect_Type4 : __ -> 'a1 **)
let rec false_rect_Type4 _ =
  assert false (* absurd case *)

(** val false_rect_Type5 : __ -> 'a1 **)
let rec false_rect_Type5 _ =
  assert false (* absurd case *)

(** val false_rect_Type3 : __ -> 'a1 **)
let rec false_rect_Type3 _ =
  assert false (* absurd case *)

(** val false_rect_Type2 : __ -> 'a1 **)
let rec false_rect_Type2 _ =
  assert false (* absurd case *)

(** val false_rect_Type1 : __ -> 'a1 **)
let rec false_rect_Type1 _ =
  assert false (* absurd case *)

(** val false_rect_Type0 : __ -> 'a1 **)
let rec false_rect_Type0 _ =
  assert false (* absurd case *)

(** val not_rect_Type4 : (__ -> 'a1) -> 'a1 **)
let rec not_rect_Type4 h_nmk =
  h_nmk __

(** val not_rect_Type5 : (__ -> 'a1) -> 'a1 **)
let rec not_rect_Type5 h_nmk =
  h_nmk __

(** val not_rect_Type3 : (__ -> 'a1) -> 'a1 **)
let rec not_rect_Type3 h_nmk =
  h_nmk __

(** val not_rect_Type2 : (__ -> 'a1) -> 'a1 **)
let rec not_rect_Type2 h_nmk =
  h_nmk __

(** val not_rect_Type1 : (__ -> 'a1) -> 'a1 **)
let rec not_rect_Type1 h_nmk =
  h_nmk __

(** val not_rect_Type0 : (__ -> 'a1) -> 'a1 **)
let rec not_rect_Type0 h_nmk =
  h_nmk __

(** val not_inv_rect_Type4 : (__ -> __ -> 'a1) -> 'a1 **)
let not_inv_rect_Type4 h1 =
  let hcut = not_rect_Type4 h1 in hcut __

(** val not_inv_rect_Type3 : (__ -> __ -> 'a1) -> 'a1 **)
let not_inv_rect_Type3 h1 =
  let hcut = not_rect_Type3 h1 in hcut __

(** val not_inv_rect_Type2 : (__ -> __ -> 'a1) -> 'a1 **)
let not_inv_rect_Type2 h1 =
  let hcut = not_rect_Type2 h1 in hcut __

(** val not_inv_rect_Type1 : (__ -> __ -> 'a1) -> 'a1 **)
let not_inv_rect_Type1 h1 =
  let hcut = not_rect_Type1 h1 in hcut __

(** val not_inv_rect_Type0 : (__ -> __ -> 'a1) -> 'a1 **)
let not_inv_rect_Type0 h1 =
  let hcut = not_rect_Type0 h1 in hcut __

(** val and_rect_Type4 : (__ -> __ -> 'a1) -> 'a1 **)
let rec and_rect_Type4 h_conj =
  h_conj __ __

(** val and_rect_Type5 : (__ -> __ -> 'a1) -> 'a1 **)
let rec and_rect_Type5 h_conj =
  h_conj __ __

(** val and_rect_Type3 : (__ -> __ -> 'a1) -> 'a1 **)
let rec and_rect_Type3 h_conj =
  h_conj __ __

(** val and_rect_Type2 : (__ -> __ -> 'a1) -> 'a1 **)
let rec and_rect_Type2 h_conj =
  h_conj __ __

(** val and_rect_Type1 : (__ -> __ -> 'a1) -> 'a1 **)
let rec and_rect_Type1 h_conj =
  h_conj __ __

(** val and_rect_Type0 : (__ -> __ -> 'a1) -> 'a1 **)
let rec and_rect_Type0 h_conj =
  h_conj __ __

(** val and_inv_rect_Type4 : (__ -> __ -> __ -> 'a1) -> 'a1 **)
let and_inv_rect_Type4 h1 =
  let hcut = and_rect_Type4 h1 in hcut __

(** val and_inv_rect_Type3 : (__ -> __ -> __ -> 'a1) -> 'a1 **)
let and_inv_rect_Type3 h1 =
  let hcut = and_rect_Type3 h1 in hcut __

(** val and_inv_rect_Type2 : (__ -> __ -> __ -> 'a1) -> 'a1 **)
let and_inv_rect_Type2 h1 =
  let hcut = and_rect_Type2 h1 in hcut __

(** val and_inv_rect_Type1 : (__ -> __ -> __ -> 'a1) -> 'a1 **)
let and_inv_rect_Type1 h1 =
  let hcut = and_rect_Type1 h1 in hcut __

(** val and_inv_rect_Type0 : (__ -> __ -> __ -> 'a1) -> 'a1 **)
let and_inv_rect_Type0 h1 =
  let hcut = and_rect_Type0 h1 in hcut __

(** val r0 : 'a1 -> 'a1 **)
let r0 t =
  t

(** val r1 : 'a1 -> 'a2 -> 'a1 -> 'a2 **)
let r1 x h_refl x_19 =
  eq_rect_Type0 x h_refl x_19

(** val r2 : 'a1 -> 'a2 -> 'a3 -> 'a1 -> 'a2 -> 'a3 **)
let r2 a0 a1 a2 b0 b1 =
  eq_rect_Type0 (r1 a0 a1 b0) (r1 a0 a2 b0) b1

(** val r3 : 'a1 -> 'a2 -> 'a3 -> 'a4 -> 'a1 -> 'a2 -> 'a3 -> 'a4 **)
let r3 a0 a1 a2 a3 b0 b1 b2 =
  eq_rect_Type0 (r2 a0 a1 a2 b0 b1) (r2 a0 a1 a3 b0 b1) b2

(** val r4 :
    'a1 -> 'a2 -> 'a3 -> 'a4 -> 'a5 -> 'a1 -> 'a2 -> 'a3 -> 'a4 -> 'a5 **)
let r4 a0 a1 a2 a3 a4 b0 b1 b2 b3 =
  eq_rect_Type0 (r3 a0 a1 a2 a3 b0 b1 b2) (r3 a0 a1 a2 a4 b0 b1 b2) b3

(** val streicherK : 'a1 -> 'a2 -> 'a2 **)
let streicherK t h =
  eq_rect_Type3_r __ h __