Exercise 7.10
As Exercise 7.9:
$$\begin{gather} ∀_{x∈S}(P(x) ⇒Q(x)) \\ \\ ⇒ \\ \\ ∀_{y∈S}(P(y) ⇒R(y)) \\ \\ ⇒ \\ \\ ∀_{z∈S}(P(z) ⇒(Q(z)∧R(z))) \end{gather}$$
The following is a first order natural deduction.
The corresponding type is
$$ (\Pi x:S.(Px \to Qx)) \to (\Pi y:S.(Py \to Ry)) \to (\Pi z:S.(Pz \to (\Pi C:*.((Qz \to Rz \to C) \to C)))) $$
with a context of $S:*, \; P, Q,R, : S \to*$.The following is a flag-style derivation in λC.
