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