2. s: T List
3. 0 < 0
nil ~ (firstn(-1;nil) @ [nil[(-1)]])2. s: T List
3. u: T
4. v: T List
5. 0 < ||v||
(v ~ (firstn(||v||-1;v) @ [v[(||v||-1)]]))6. 0 < ||v||+1
[u / v] ~ (firstn(||v||+1-1;[u / v]) @ [[u / v][(||v||+1-1)]])
T:Type, s:T List. 0 < ||s|| (s ~ (firstn(||s||-1;s) @ [s[(||s||-1)]]))
| 1 | 1. T: Type 2. s: T List 3. 0 < 0 nil ~ (firstn(-1;nil) @ [nil[(-1)]]) | Auto |
| 2 | 1. T: Type 2. s: T List 3. u: T 4. v: T List 5. 0 < ||v|| (v ~ (firstn(||v||-1;v) @ [v[(||v||-1)]]))6. 0 < ||v||+1 [u / v] ~ (firstn(||v||+1-1;[u / v]) @ [[u / v][(||v||+1-1)]]) | 9 steps |
About:
 |  |  |  |  |  |
 |  |  |  |  |  |  |