The library directory lib_prop contains four subdirectories lib_bool, lib_sum, lib_nat and lib_list. Each of these directories contains a single file lib_bool.l etc. These files contain the same theorems as the corresponding files in the main library. They are for using impredicative (in Prop) datatypes with elimination over Prop. Under this framework it is not provable that true is not equal to false and similar results for other datatypes. It is normal to assume these results. These files all depend on lib_bool which contains true_not_false as an assumption. This assumption is used in the other files to prove those theorems which require it. See section 3 (particularly the final paragraph) for how to use these files in conjunction with the rest of the library.