Keep numbered existential names distinct from other existential names
Why
A numbered name can equal the base name of another existential, as $a1 for the second 'a and for 'a1, and the printer then falls back to internal name/stamp names. Names already given in the binding are now skipped.
modifiedDiagnostic comparing existentials
type rec a2 = A2('a): a2type rec a1 = A1('a1): a1type rec a3 = A3('a): a3let f = (A2(y), A1(x), A3(z)) => z == x
text
Before
After
This has type: \"$a1/1011"But it's being compared to something of type: \"$a1/1013"This has type: $a1But it's being compared to something of type: $a2