P:(Alph*
Prop).
(n:
. (l:Alph*. ||l|| < n 
P(l)) (l:Alph*. ||l|| = n P(l)))
(l:Alph*. P(l))
auto2_list_ind
0 ; a.as' ||as'||+1 (recursive)
Thm* P:(Alph*Prop).
(n:. (l:Alph*. ||l|| < n P(l)) (l:Alph*. ||l|| = n P(l)))
(l:Alph*. P(l))
auto2_list_ind
In prior sections: list 1