n:{1...}, m:{n+1...}, f:(
m
n). 
i,j:m. i < j & f(i) = f(j) phole_lemma
} == {k:
| i 
k < j }
Thm* n:{1...}, m:{n+1...}, f:(mn). i,j:m. i < j & f(i) = f(j) phole_lemma
Thm* n:{1...}, f:((n+1)n). i:(n+1), j:i. f(i) = f(j) phole_aux
Thm* n:, T:Type, B:(TProp).
(n ~ T) & (t:T. Dec(B(t))) 
(m:. m ~ {t:T| B(t) })
fin_dec_fin
Thm* n:
, x:(n
n). (x 
n) < n div_bounds_2
Thm* Fin(T) 
(m:. m ~ T) fin_iff_1_1_nsub
Thm* n:. Fin(n) nsub_is_finite
Thm* n,m:. f:(n
m(nm)). Bij(nm; (nm); f) rect_enumer