Exercise 7.4
Give λC-derivations to show that the following natural deduction rules are derivable in λC (cf. Section 7.2,I):
(a) (∧-elim-left-sec),
(b) (∧-elim-right-sec).
(a) The (∧-elim-left-sec) rule is, in second order,
$$\frac{\Pi C : ∗. (A \to B \to C) \to C}{A}$$
Our task is to find $?_2$ in the type theoretic version of this rule,
$$ \frac{\Gamma \vdash c : \Pi C : *. (A \to B\to C) \to C}{\Gamma \vdash ?_2 :A} $$
That is, given the context that the conjunction holds, we need to show that $A$ holds by finding an inhabitant.
The following is a λC derivation, showing that
$$cA(\lambda x:A.\lambda y:B.x)$$
inhabits $A$ as a result of the given context which includes an encoding of the conjunction.
(b) The task for the (∧-elim-left-sec) rule is, in second order,
$$\frac{\Pi C : ∗. (A \to B \to C) \to C}{B}$$
Our task is to find $?_2$ in the type theoretic version of this rule,
$$ \frac{\Gamma \vdash c : \Pi C : *. (A \to B\to C) \to C}{\Gamma \vdash ?_2 :B} $$
The following is a λC derivation, showing that
$$cB(\lambda x:A.\lambda y:B.y)$$
inhabits $B$ as a result of the given context which includes an encoding of the conjunction.
