DEFINITION True_rect()
TYPE =
       ΠP:(Type:593:cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/True_rect.con)
         .P→True→P
BODY =
Show proof