feat(tactic/lint): improve check_univs linter (#9698)
* `check_univs` now only checks the type of `d` and ignores `d._proof_i` subterms
* move `expr.univ_params_grouped` to the linter file (it seems increasingly unlikely that this has a use in other applications)
* We now don't test automatically generated declarations anymore.
Co-authored-by: Johan Commelin <johan@commelin.net>
