DEFINITION B_rect()
TYPE =
       ΠP:B
                →(Type:90614:cic:/matita/LAMBDA-TYPES/LambdaDelta-1/T/defs/B_rect.con)
         .(P Abbr)→(P Abst)→(P Void)→Πb:B.(P b)
BODY =
λP:B
               →(Type:90614:cic:/matita/LAMBDA-TYPES/LambdaDelta-1/T/defs/B_rect.con)
         .λp:P Abbr.λp1:P Abst.λp2:P Void.λb:B.<P> CASE b OF Abbr⇒p | Abst⇒p1 | Void⇒p2