Post #2191764

By the way, every untyped *normal* term can be typed in system F (for example λx. xx can be given the type Unit -> Unit where Unit = forall T. T -> T). And as a corollary, there exists an interpreter of system F in untyped lambda calculus operating on Godel encoded Church numerals, that can be given a type in system F itself.