2. s: T List
3.
i,j:
. i < ||s|| 
j < ||s|| 
i = j s[i] = s[j]4. a1:
||s||5. a2:
||s||6. s[a1] = s[a2]
7.
a1 = a2
a1 = a2
T:Type, s:T List. no_repeats(T;s) (
f:(||s||
T). Inj(||s||; T; f))
i.s[i]]
| 1 | 1. T: Type 2. s: T List 3. i,j:. i < ||s|| j < ||s|| i = j s[i] = s[j]4. a1: ||s||5. a2: ||s||6. s[a1] = s[a2] 7. a1 = a2 a1 = a2 | 1 step |
About:
 |  |  |  |  |  |  |  |  |