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 =
λP:bool
               →(Type:2563:cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/bool_rect.con)
         .λp:P true.λp1:P false.λb:bool.<P> CASE b OF true⇒p | false⇒p1