Exercise 4.4
Give shortened λω-derivations in flag format of the following judgements:
(a) $α : ∗, β : ∗→∗ \; ⊢ \; β(βα) : ∗$
(b) $α : ∗, β : ∗→∗, x : β(βα) \; ⊢ \; λy : α. x : α →β(βα)$
(c) $∅ \; ⊢ \; λα : ∗. λβ : ∗→∗. β(βα) : ∗→(∗→∗) →∗$
(d) $∅ \; ⊢ \; (λα : ∗. λβ : ∗→∗. β(βα)) \; nat \; (λγ : ∗. γ) : ∗$, assuming that $nat$ is a constant of type $∗$.
(a) The following shows both the full and shortened derivation.
(b) The following is a shortened derivation.
(c) The following is a shortened derivation.
(d) The following is a shortened derivation.
