let id = λ(X : Type) → X in < x : id Bool | z >