[User23]

Similarly forall f x=y => f(x)=f(y) can do quite a lot of work given that you’re free to choose any convenient f and then substitute its body.