Bug with letter H?

Stream: new members

[Li Yao'an]

Consider the following code:

structure X :=
mk :: (adj : Prop)

constant S: set ℕ

def th1 (K : X) :=
        ∀ e ∈ S, K.adj

def th2 (H : X) :=
        ∀ e ∈ S, H.adj

def th3 (Q : X) :=
        ∀ e ∈ S, Q.adj

Is there a reason why Lean (online editor/VS) only throws an error for th2 when the letter H is used? This looks like a bug to me.

[Kenny Lau]

∀ e ∈ S is sugar for ∀ e, ∀ H : e ∈ S

[Kevin Buzzard]

Good catch

[Kenny Lau]

I just read the error message

[Li Yao'an]

Thanks for the reply. It makes sense now!