chore: simplify is_rec / is_reflexive

[digama0]

• The find call in is_rec was just a complicated way to write the has_ind_occ function defined just afterwards. By using it, is_rec and is_reflexive are made much more clearly similar.
• fixed a typo
• is_reflexive was using instantiate but is_rec was not. None of the functions involved require closed terms, and replacing a bvar with an fvar does not change the result of is_pi or has_ind_occ, so the instantiate is unnecessary and can be removed (although I doubt it is a measurable perf difference). As a bonus it is now structurally recursive, which is advantageous for a certain project I'm working on...

[leanprover-community-mathlib4-bot]

• ✅ Mathlib branch lean-pr-testing-2674 has successfully built against this PR. (2023-10-12 13:59:40) View Log