dedup first occurrence

Stream: new members

[Bjørn Kjos-Hanssen]

I have this:

u v: vector (fin b) t
u v: vector (fin 1) t

When I do dedup it changes the last occurrences of u, v to u_1, v_1. Is there a way to change the first occurrences instead?

[Kevin Buzzard]

Why do you even have that? Having different things with the same names is confusing.

[Kevin Buzzard]

Can you avoid having it?

[Bjørn Kjos-Hanssen]

I have a proof hb: b=1 so I did rw hb at u, rw hb at v

[Ruben Van de Velde]

What happens if you do subst hb instead?

[Bjørn Kjos-Hanssen]

Ah! That does it, thanks I didn't know about subst.