DEFINITION True_rect()
TYPE =
       ΠP:(Type:593:cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/True_rect.con)
         .P→True→P
BODY =
λP:(Type:593:cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/True_rect.con)
         .λp:P.λH:True.<λH1:True.P> CASE H OF I⇒p