L:
List, i:||L||. 0 < L[i] 
||L[i--]|| = ||L|| 
n:, f:(n
T). ||mklist(n;f)|| = n | Rank | Theorem | Name |
| 2 | Thm* L: List, i:||L||. 0 < L[i] ||L[i--]|| = ||L|| | [list-dec-length] |
| cites | ||
| 1 | Thm* n:, f:(nT). ||mklist(n;f)|| = n | [mklist_length] |