L:T List, P:(T
). (x
L.P(x)) 
(i:
||L||. P(L[i]))a:T, as:T List, i:
. 0 < i 
i
||as|| [a / as][i] = as[(i-1)]| Theorem | Name |
| Thm* L:T List, P:(T). (xL.P(x)) (i:||L||. P(L[i])) | [assert_l_ball] |
| cites | |
| Thm* a:T, as:T List, i:. 0 < i i||as|| [a / as][i] = as[(i-1)] | [select_cons_tl] |