Incorrect `fun {a}` linter

Stream: lean4

[Mario Carneiro]

I think a useful linter would be to detect when the proof uses fun {a} => to introduce a variable when fun a => would also have worked. This is usually masking a definition mismatch when you change a forall from implicit to explicit, and the reverse problem (using fun a => where fun {a} => is expected) is a lot worse since it can make variable names not match up