In order to do that, we need to quantify over non-expansive
predicates instead of arbitrary predicates.