2. L: T List
3. u: T
4. v: T List
5. no_repeats(T;rev(v))
no_repeats(T;v)
no_repeats(T;rev(v) @ [u]) no_repeats(T;[u / v])
T:Type, L:T List. no_repeats(T;rev(L)) no_repeats(T;L)
| 1 | 1. T: Type 2. L: T List 3. u: T 4. v: T List 5. no_repeats(T;rev(v)) no_repeats(T;v) no_repeats(T;rev(v) @ [u]) no_repeats(T;[u / v]) | 2 steps |
About:
 |  |  |  |  |  |