(S ~ T) one_one_sym
f:(A
B), g:(BA). InvFuns(A; B; f; g)
Thm* (T ~ S) (S ~ T) one_one_sym
Thm* Fin(T) & (T ~ S) Fin(S) one_one_preser_fin
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* (T ~ U) & Fin(T) Fin(U) one2one_preserves_fin
In prior sections: fun 1