Термин t можно ввести, если существует контекст Γ и тип τ такой, что суждение
"Γ ⊦ t: τ" выводимо.
Как мне указать, является ли выражение "\ f -> \ x -> f (f (f x))" типографским или нет?
А кто-нибудь может мне объяснить, что такое нормальные и нейтральные формы лам?
Спасибо