Thm* f:(AB). (A ~ B) & Fin(B) Surj(A; B; f) Inj(A; B; f) surj_is_inj_gen

Thm* n:, f:(nn). Surj(n; n; f) Inj(n; n; f) surj_is_inj

Thm* Auto:Automata(Alph;St), c:(StAlph*). (q:St. (Result(Auto)c(q)) = q) & Fin(Alph) & Fin(St) Surj(St; x,y:Alph*//(x LangOf(Auto)-induced Equiv y); c) homo_is_surj