Pを集合として表現していいなら、存在型の表記は { ∃X where X: P, X } より { ∃X ∈ P, X } のほうがいいかもなって思った