Tagged encoding of a finite tuple ($(a_i{)}_{i=1}^n⟼\{⟨t_i,a_i⟩:1\le i\le n\}$)

Using distinct fixed tags $t_1,\dots ,t_n$, encode a tuple $(a_1,\dots ,a_n)$ by the set $\{⟨t_i,a_i⟩:1\le i\le n\}$. Injectivity of the ordered-pair construction makes the unique member with first coordinate $t_i$ recover $a_i$. Thus a set can retain the order of a finite tuple when its entries are tagged, even if some coordinates coincide.