variable H bug with `∀ h ∈ H`

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
    • Specifically, check out the wishlist, open RFCs,
      or feature requests.
  • Reduced the issue to a self-contained, reproducible test case.

Description

Apologies -- I suspect this is well-known but I couldn't find it in the issues. If a user has a variable H (and this is a common name for a group in mathsworld) then bounded quantifiers can cause problems, I think because the parser might be introducing another variable H.

Steps to Reproduce

class normal {G : Type*} [group G] (H : set G) :=
(conjugate : ∀ g : G, ∀ h ∈ H, g * h * g⁻¹ ∈ H)

Expected behavior: [What you expect to happen]

Success (which one can obtain by changing the H's to K's)

Actual behavior: [What actually happens]

type mismatch at application
  g * h * g⁻¹ ∈ H
term
  H
has type
  h ∈ H : Prop
but is expected to have type
  ?m_1 : Type ?

Reproduces how often: [What percentage of the time does it reproduce?]

100%

Versions

3.5.1, Ubuntu 18.04

Additional Information

Any additional information, configuration or data that might be necessary to reproduce the issue.

Start by reproducing the class declaration in the issue on the reported Lean 3.5.1 setup, then compare it with the version that replaces H with K. Investigate how bounded quantifiers are parsed and scoped; done means the original declaration succeeds without changing the variable names and a regression test covers it.