[Hol-info] hol-light , is this a bug of BETA_CONV

[hao d. <den...@gm...>]

Hi, there:
    I'm a new user of hol-light and I find the following thing strange :

# BETA_CONV `(\x. ?y. x = a /\ y = b) y`;;
Warning: inventing type variables
val it : thm = |- (\x. ?y. x = a /\ y = b) y <=> (?y. y = a /\ y = b)

the ?y is not renamed in the substitution , is this a bug ?
or am I wrong at some where?


Thanks in advance.