DEFINITION F_rect()
TYPE =
       ΠP:F
                →(Type:90896:cic:/matita/LAMBDA-TYPES/LambdaDelta-1/T/defs/F_rect.con)
         .(P Appl)→(P Cast)→Πf:F.(P f)
BODY =
Show proof