Parameters of an inductive clash with binders of constructor

[mtzguido]

trafficstars

module Bug

noeq
type ty #a (x:a) =
  | I : (a:nat) -> ty x

let _ = assert (forall x. x + 1 > x) // just here to trigger a query

This gives:

Bug.fst(7,0-7,36): (Error 276) queries-Bug.smt2: Unexpected output from Z3: (error "line 153692 column 33: invalid declaration, function 'Bug.I_a' (with the given signature) already declared")
(error "line 153979 column 33: named expression already defined") 

since there are two projectors for a (named I_a in the encoding) being defined. This is not triggered too commonly I believe, since it requires a being an implicit. I think we could just forbid repeated names, but maybe better if we can give these projectors different names in the encoding.