--- presupposes logic.occ

( bool : Type )

---

( true : bool )
( false : bool )

---

( not : bool -> bool )
( not_ax_1 : !! ((not false) = true) )
( not_ax_2 : !! ((not true) = false) )

---

( and : bool -> bool -> bool )
( and_ax_1 : !! {b : bool} ((and false b) = false) )
( and_ax_2 : !! {b : bool} ((and b false) = false) )
( and_ax_3 : !! {b : bool} ((and true true) = true) )

---

( or : bool -> bool -> bool )
( or_ax_1 : !! {b : bool} ((or true b) = true) )
( or_ax_2 : !! {b : bool} ((or b true) = true) )
( or_ax_3 : !! {b : bool} ((or false false) = false) )

---

( xor : bool -> bool -> bool )
( xor_ax_1 : !! {b : bool} ((xor true b) = (not b)) )
( xor_ax_2 : !! {b : bool} ((xor b true) = (not b)) )
( xor_ax_3 : !! {b : bool} ((xor false b) = b) )
( xor_ax_4 : !! {b : bool} ((xor b false) = b) )
( xor_ax_5 : !! {b : bool} ((xor b b) = false) )

---

( bool_elim : {U | UNIV}{T : bool -> U}(T true) -> (T false) -> {b : bool} (T b) )

( bool_elim_ax_true : !! {T : bool -> Type}{t : (T true)}{f : (T false)}
                          ((bool_elim T t f true) = t) )

( bool_elim_ax_false : !! {T : bool -> Type}{t : (T true)}{f : (T false)}
                           ((bool_elim T t f false) = f) )

---

( bool_rec := [T | Type] (bool_elim ([_ : bool] T))
           : {T | Type} T -> T -> bool -> T )

( bool_ind := [P : bool -> Prop] (bool_elim P)
           : {P : bool -> Prop}(P true) -> (P false) -> {b : bool} (P b) )

---

( bool_true_not_eq_false : (Not (true = false)) )

( done )