Exercise 7.12
(a) Complete the derivation given in Section 7.5 that shows that the natural deduction rule (∃-intro-sec) is derivable in λC.
(b) Give a flag-style λC-derivation verifying the following tautology of classical logic:
$$¬∃_{x∈S}(¬P(x)) ⇒ ∀_{y∈S}(P(y))$$
(Hint: use part (a) and DN.)
(a) The natural deduction rule (∃-intro-sec) is.
$$ \frac{a : S \quad \quad P a}{\Pi \alpha :*. ((\Pi x : S. (P x \to \alpha)) \to \alpha)} $$
The following is a derivation in λC.
(b) The corresponding type is
$$ (\Pi \alpha :*. ((\Pi x : S. ((P x \to \bot)\to \alpha)) \to \alpha ) \to \bot ) \; \to \; \Pi y:S.Py $$
The following is a derivation in λC.
