Exercise 5.6
Prove that $(A ⇒(A ⇒B)) ⇒(A ⇒B)$ is a tautology, (first) in natural deduction and (second) by means of a shortened λP-derivation.
Natural Deduction
The following is a natural deduction proof of the logical statement.
Full λP Derivation
Noting that the associated type for $A \implies B$ is $\Pi x:A.B$, then the type for the given logical statement is
$$\Pi z:(\Pi y:A.(\Pi x:A.B)) . (\Pi x:A.B)$$
By inspection, a term that inhabits that type is
$$\lambda z:(\Pi y:A.(\Pi x:A.B)). (\lambda x:A. zxx)$$
The following is a full derivation, before we develop a shorted one below (click to enlarge).
Shortened λP Derivation
The following is a shortened derivation.
