THM	not_dec_is_dec	A:. P:A . (x:A. P x (P x)) ((x:A. (P x)) (x:A. (P x))) (x:A. P x) (x:A. P x)
THM	rect_enumer	n,m:. f:(n m) (n * m). Bij(n m;(n * m);f)
DISP	finite_df	Fin(<s:s:*>)== Fin(<s>)
ABS	finite	Fin(s) == n:. f:n s. Bij(n;s;f)
THM	finite_wf	T:. Fin(T)
THM	comb_for_finite_wf	(T,z.Fin(T)) T: True
THM	nsub_is_finite	n:. Fin(n)
THM	bool_is_finite	Fin()
THM	one2one_preserves_fin	T,U:. 1-1-Corresp(T;U) Fin(T) Fin(U)
THM	fin_iff_1_1_nsub	T:. Fin(T) (m:. 1-1-Corresp(m;T))
THM	fun_enumer	n,m:. f:(m n) (nm). Bij(m n;(nm);f)
THM	fun_preserves_fin	S,T:. Fin(S) Fin(T) Fin(S T)
THM	auto2_list_ind	Alph:. P:Alph List . (n: (l:Alph List. ||l|| < n P l) (l:Alph List. ||l|| = n P l)) (l:Alph List. P l)
THM	auto2_lemma_0	T:. P:T . (x:T. Dec(P x)) Dec(x:T. (P x)) Dec(x:T. P x)
THM	auto2_lemma_1	T:. P,Q:T . (t:T. P t Q t) 1-1-Corresp({t:T| P t} ;{t:T| Q t} )
THM	auto2_lemma_3	Alph:. R:Alph List Alph List . n:. (x:Alph List. R x x) (x,y:Alph List. R x y R y x) (x,y,z:Alph List. R x y R y z R x z) (x,y,z:Alph List. R x y R (z @ x) (z @ y)) (w:n Alph List. l:Alph List. i:n. R l (w i)) (a,b,c:Alph List. ||a|| n * n (a':Alph List ||a'|| < ||a|| R (a @ b) (a' @ b) R (a @ c) (a' @ c)))
THM	auto2_lemma_4	Alph:. R:Alph List Alph List . n:. (x:Alph List. R x x) (x,y:Alph List. R x y R y x) (x,y,z:Alph List. R x y R y z R x z) (x,y,z:Alph List. R x y R (z @ x) (z @ y)) (w:n Alph List. l:Alph List. i:n. R l (w i)) (a,b,c:Alph List. a':Alph List ||a'|| < n * n R (a @ b) (a' @ b) R (a @ c) (a' @ c))
THM	auto2_lemma_5	Alph:. n:. Fin(Alph) Fin({l:Alph List| ||l|| = n} )
THM	auto2_lemma_6	T:. R:T . Fin(T) (t:T. Dec(R t)) Dec(t:T. R t)
THM	auto2_lemma_7	Alph:. R:Alph List Alph List . n:. L:Alph List . m:. (x:Alph List. R x x) (x,y:Alph List. R x y R y x) (x,y,z:Alph List. R x y R y z R x z) (x,y,z:Alph List. R x y R (z @ x) (z @ y)) (w:n Alph List. l:Alph List. i:n. R l (w i)) (v:m Alph List. l:Alph List. (L l) (i:m. R l (v i))) Fin(Alph) (x,y:Alph List. Dec(l:Alph List. L (l @ x) = L (l @ y)))
THM	auto2_lemma_8	Alph:. R:Alph List Alph List . n:. L:Alph List . m:. (x:Alph List. R x x) (x,y:Alph List. R x y R y x) (x,y,z:Alph List. R x y R y z R x z) (x,y,z:Alph List. R x y R (z @ x) (z @ y)) (w:n Alph List. l:Alph List. i:n. R l (w i)) (v:m Alph List. l:Alph List. (L l) (i:m. R l (v i))) Fin(Alph) (x,y:Alph List. Dec(l:Alph List. L (l @ x) = L (l @ y)))

the other theories