This way type class inference is not invokved when used in tactics
like iPvs while not having to write an @.

(Idea suggested by Ralf.)