(λ(x : X) → x) y