let id = λ(X : Type) → X in λ(T : Type) → { a : id Bool, b : T }