W dniu 08.02.2021 o 19:56, Uwe Nestmann pisze: > is there any publication that contains a reasonably formal “direct" argument/proof why \Omega = \omega\omega is_not_ Curry-typable in System F? ------------- Dear Uwe, this is Exercise 11.16 in Sorensen-Urzyczyn: Lectures on the Curry-Howard Isomorphism. Best regards, Paweł Urzyczyn