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

val bool_rect_Type5 : 'a1 -> 'a1 -> bool -> 'a1

val bool_rect_Type3 : 'a1 -> 'a1 -> bool -> 'a1

val bool_rect_Type2 : 'a1 -> 'a1 -> bool -> 'a1

val bool_rect_Type1 : 'a1 -> 'a1 -> bool -> 'a1

val bool_rect_Type0 : 'a1 -> 'a1 -> bool -> 'a1

val bool_inv_rect_Type4 : bool -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val bool_inv_rect_Type3 : bool -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val bool_inv_rect_Type2 : bool -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val bool_inv_rect_Type1 : bool -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val bool_inv_rect_Type0 : bool -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val bool_discr : bool -> bool -> __

val notb : bool -> bool

val andb : bool -> bool -> bool

val orb : bool -> bool -> bool

val xorb : bool -> bool -> bool