Exercise 5.5
Prove that $A ⇒ ((A ⇒ B) ⇒ B)$ is a tautology by giving a shortened λP-derivation.
To show that $A ⇒ ((A ⇒ B) ⇒ B)$ is a tautology, we need to show that corresponding type is derivable and is also inhabited.
Full Derivation
The following is a flag notation derivation of both the type and the inhabitant. This is a full derivation before we develop a shortened derivation.
Shortened Derivation
The following is a shortened derivation.
