Exercise 7.13
Verify that the following expression is a tautology in constructive logic, by giving a flag-style derivation in λC:
$$ \exists_{x \in S}(P(x)) \quad \implies \quad ( \; \forall_{y \in S}(P(y) \implies Q(y)) \implies \exists_{z \in S}(Q(z)) \; ) $$
Before we develop a derivation in λC it is educational to develop a natural deduction proof, because it will guide the λC derivation.
This answer on stack exchange is a helpful explanation of intro and elim rules for ∃ and ∀.
The corresponding type is
$$ \Pi \alpha : * . ((\Pi x : S. (P x \to \alpha )) \to \alpha) \quad \to \quad \Pi y:S.(Py \to Qy) \quad \to \quad \Pi \alpha : * . ((\Pi z : S. (Q z \to \alpha )) \to \alpha) $$
The following is a derivation in λC.
