(λ(x : X) → y) x