The file lib_bool gives the basic definition of the boolean type with its recursor and induction principle and propositional functions is_true and is_false which are used in the two characterisation theorems that true is not equal to false and that any boolean is either true or false.
** Module lib_bool Imports lib_eq_basics $bool : Type(bool) $true : bool $false : bool $bool_elim : {C_bool:bool->TYPE}(C_bool true)->(C_bool false)->{z:bool}C_bool z [[C_bool:bool->TYPE][f_true:C_bool true][f_false:C_bool false] bool_elim C_bool f_true f_false true ==> f_true || bool_elim C_bool f_true f_false false ==> f_false] bool_rec = ... : {T|Type}T->T->bool->T bool_ind = ... : {P:bool->Prop}(P true)->(P false)->{b:bool}P b bool_double_elim = ... : {T:bool->bool->Type}(T true true)->(T true false)->(T false true)-> (T false false)->{x,y:bool}T x y is_true = ... : bool->Prop is_false = ... : bool->Prop true_not_false = ... : not (Eq true false) true_or_false = ... : {b:bool}or (is_true b) (is_false b)