DEFINITION bool_rect()
TYPE =
       ΠP:bool
                →(Type:2563:cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/bool_rect.con)
         .(P true)→(P false)→Πb:bool.(P b)
BODY =
Show proof