DEFINITION F_rec()
TYPE =
       ΠP:F→Set.(P Appl)→(P Cast)→Πf:F.(P f)
BODY =
λP:F→Set.λp:P Appl.λp1:P Cast.λf:F.<P> CASE f OF Appl⇒p | Cast⇒p1