[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Perhaps it helps to solve the following simpler exercise first: Is there a term G : (nat → nat) → nat such that, for any closed term f : nat → nat, G f is a Gödel code of f ? With kind regards, Andrej
