P:(Alph*
Prop).
(n:
. (l:Alph*. ||l|| < n 
P(l)) (l:Alph*. ||l|| = n P(l)))
(l:Alph*. P(l))
auto2_list_ind
== {i:
| 0
i }
Thm* P:(Alph*Prop).
(n:. (l:Alph*. ||l|| < n P(l)) (l:Alph*. ||l|| = n P(l)))
(l:Alph*. P(l))
auto2_list_ind
Thm* n:, T:Type, B:(TProp).
(n ~ T) & (t:T. Dec(B(t))) (
m:. m ~ {t:T| B(t) })
fin_dec_fin
Thm* Fin(T) 
(m:. m ~ T) fin_iff_1_1_nsub
Thm* n:. Fin(n) nsub_is_finite