generalized existentialは、それに加えてユーザ側での型の扱いがあるので、その次の段階になりそう。