Name-shadowing in auto-generated names for injection tactic

[bmsherman]

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

Consider the following example:

lemma foo (x y x' y' : ℕ) 
  (h : (x, y) = (x', y'))
  : false
:= begin
injection h,
end

Actual behavior:
After applying the injection tactic, the proof state looks like this:

x y x' y' : ℕ,
h : (x, y) = (x', y'),
h : x = x',
h : y = y'
⊢ false

Expected behavior: I would expect that the injection tactic (when given an insufficient supply of "manual" names) would generate names that are "fresh", i.e., not already in context.

Versions

I am using Lean version from August 12, 2017, Lean (version 3.2.1, commit 32ddac5, Release).

Additional Information

The relevant code that must be changed in the injection tactic can be found here:
https://github.com/leanprover/lean/blob/5a2b7348f9d042a6e7e921f66440d884bb897f33/library/init/meta/injection_tactic.lean#L21

We discussed this on the Lean Gitter and @digama0 suggested the behavior of using names h_n:
https://gitter.im/leanprover_public/Lobby?at=59962766ee5c9a4c5fd0c896

[digama0]

I can PR a fix for this, but I'd like word from the devs that this is worth it first.