Exercise 3.11
Take $⊥$as in Exercise 3.5. Prove that the following term is legal in the empty context:
$$ λx : ⊥. x(⊥→⊥→⊥)(x(⊥→⊥)x)(x(⊥→⊥→⊥)xx) $$
What is its type?
Let's remind ourselves of $⊥$,
$$ ⊥ \equiv Πα:*.α $$
This tells us $x$ is a function that takes a type as argument, and returns an object of that type.
The following flag format derivation considers the 3 sub-terms in the longer term: $x(⊥→⊥→⊥)$, $(x(⊥→⊥)x)$, and $(x(⊥→⊥→⊥)xx)$ separately, before combining them.
We have derived the term and it has a type $⊥→⊥x$ in the empty context, so is legal.
