Exercise 7.7
Give λC-derivations to show that the following natural deduction rules are derivable in λC:
(a) (∨-intro-left-sec)
(b) (∨-intro-right-sec)
(a) The (∨-intro-left-sec) rule is
$$\frac{A}{\Pi C:*.(A \to C) \to (B \to C) \to C}$$
The following is a λC derivation of this rule.
(b) The (∨-intro-right-sec) rule is
$$\frac{B}{\Pi C:*.(A \to C) \to (B \to C) \to C}$$
The following is a λC derivation of this rule.
