Comment by tromp

An implicit K suffices for universality, as in \x\y\z. x z (y (\w.z))