I have a question about evaluating truth of the sign assemblies in Bourbaki Theory of Sets.
It's my understanding that when there are duplicate assemblies each starting with the choice operator $\tau$, this operator must choose the same value for each linked $\square$ in all duplicate assemblies. Therefore, to evaluate the truth of a sequence of signs, the sequence must be searched for duplicate sequences starting with $\tau$.
Is it documented elsewhere? I suspect this is costly, but are there advantages? Perhaps eliminating the variable name from the form so duplicates can be found?
I have yet to see any Bourbaki documentation on this and am confused by that.