Exercise 6.9
Given $S : ∗, P : S → *$ and $f : S → S$, we define in λC the expression:
$$M ≡ λx : S. ΠQ : S →*. (Πz : S. (Qz →Q(f z))) →Qx$$
Give a term of type $Πa : S. (M a →M(f a))$ and a (shortened) derivation proving this.
The following is an inhabitant of the type $\Pi a:S . (Ma \to M(fa))$
$$\lambda b:Ma . \lambda Q:S\to *.\lambda g: (\Pi z : S. (Qz \to Q(f z))).ga(bQg)$$
The following is a shortened derivation.
