(*#* Here are collected some results about the type sumbool (see INIT/Specif.v)
[sumbool A B], which is written [{A}+{B}], is the informative
(*#* Here are collected some results about the type sumbool (see INIT/Specif.v)
[sumbool A B], which is written [{A}+{B}], is the informative