let id = λ(X : Type) → X in id Bool → id Natural