L:T List, i,j:
||L||. ||swap(L;i;j)|| = ||L|| 
L:T List, f:(||L||
||L||). ||(L o f)|| = ||L|| | Rank | Theorem | Name |
| 3 | L:T List, i,j:||L||. ||swap(L;i;j)|| = ||L|| | [swap_length] |
| cites the following: | ||
| 2 | L:T List, f:(||L||||L||). ||(L o f)|| = ||L|| | [permute_list_length] |