open Preamble

open Hints_declaration

open Core_notation

open Pts

open Logic

open Relations

type bool =
| True
| False

(** val bool_rect_Type4 : 'a1 -> 'a1 -> bool -> 'a1 **)
let rec bool_rect_Type4 h_true h_false = function
| True -> h_true
| False -> h_false

(** val bool_rect_Type5 : 'a1 -> 'a1 -> bool -> 'a1 **)
let rec bool_rect_Type5 h_true h_false = function
| True -> h_true
| False -> h_false

(** val bool_rect_Type3 : 'a1 -> 'a1 -> bool -> 'a1 **)
let rec bool_rect_Type3 h_true h_false = function
| True -> h_true
| False -> h_false

(** val bool_rect_Type2 : 'a1 -> 'a1 -> bool -> 'a1 **)
let rec bool_rect_Type2 h_true h_false = function
| True -> h_true
| False -> h_false

(** val bool_rect_Type1 : 'a1 -> 'a1 -> bool -> 'a1 **)
let rec bool_rect_Type1 h_true h_false = function
| True -> h_true
| False -> h_false

(** val bool_rect_Type0 : 'a1 -> 'a1 -> bool -> 'a1 **)
let rec bool_rect_Type0 h_true h_false = function
| True -> h_true
| False -> h_false

(** val bool_inv_rect_Type4 : bool -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let bool_inv_rect_Type4 hterm h1 h2 =
  let hcut = bool_rect_Type4 h1 h2 hterm in hcut __

(** val bool_inv_rect_Type3 : bool -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let bool_inv_rect_Type3 hterm h1 h2 =
  let hcut = bool_rect_Type3 h1 h2 hterm in hcut __

(** val bool_inv_rect_Type2 : bool -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let bool_inv_rect_Type2 hterm h1 h2 =
  let hcut = bool_rect_Type2 h1 h2 hterm in hcut __

(** val bool_inv_rect_Type1 : bool -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let bool_inv_rect_Type1 hterm h1 h2 =
  let hcut = bool_rect_Type1 h1 h2 hterm in hcut __

(** val bool_inv_rect_Type0 : bool -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
let bool_inv_rect_Type0 hterm h1 h2 =
  let hcut = bool_rect_Type0 h1 h2 hterm in hcut __

(** val bool_discr : bool -> bool -> __ **)
let bool_discr x y =
  Logic.eq_rect_Type2 x
    (match x with
     | True -> Obj.magic (fun _ dH -> dH)
     | False -> Obj.magic (fun _ dH -> dH)) y

(** val notb : bool -> bool **)
let notb = function
| True -> False
| False -> True

(** val andb : bool -> bool -> bool **)
let andb b1 b2 =
  match b1 with
  | True -> b2
  | False -> False

(** val orb : bool -> bool -> bool **)
let orb b1 b2 =
  match b1 with
  | True -> True
  | False -> b2

(** val xorb : bool -> bool -> bool **)
let xorb b1 b2 =
  match b1 with
  | True ->
    (match b2 with
     | True -> False
     | False -> True)
  | False ->
    (match b2 with
     | True -> True
     | False -> False)