Thm* Fin(St) (eq:(StSt). x,y:St. eq(x,y) x = y) fin_dist_func

Thm* Fin(T) (x,y:T. Dec(x = y)) fin_is_decid

Thm* f:(TS). Fin(S) & (s:S. Dec(t:T. f(t) = s)) Fin(x,y:T//(f(x) = f(y))) inv_of_fin_is_fin

Thm* Fin(T) & (T ~ S) Fin(S) one_one_preser_fin

Thm* B:(TProp). Fin(T) & (t:T. Dec(B(t))) Fin({t:T| B(t) }) finite_decidable_subset

Thm* t:T. Fin(T) Fin(TT) prod_fin_is_fin

Thm* Fin(T) (m:. m ~ T) fin_iff_1_1_nsub

Thm* (T ~ U) & Fin(T) Fin(U) one2one_preserves_fin

Thm* Fin() bool_is_finite

Thm* n:. Fin(n) nsub_is_finite