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 =
λP:F
               →(Type:90896:cic:/matita/LAMBDA-TYPES/LambdaDelta-1/T/defs/F_rect.con)
         .λp:P Appl.λp1:P Cast.λf:F.<P> CASE f OF Appl⇒p | Cast⇒p1