Exercise 6.2
Let $Γ ≡S : ∗, P : S →∗, A : ∗$.
Prove by means of a flag derivation that the following expression is inhabited in λC with respect to Γ:
$$(Πx : S. (A →P x)) →A →Πy : S. P y$$
(You may shorten the derivation, as explained in Section 4.5.)
By inspection, the following should be an inhabitant of the given type.
$$\lambda f:(\Pi x:S.(A \to P x)) . \lambda a:A . \lambda y:S . fya$$
The following is a shortened flag derivation using λC rules.
