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 =
Show proof