Thm* n:{1...}, A:Type, L:LangOver(A), R:(A*A*Prop). Fin(A) (EquivRel x,y:A*. x R y) (n ~ (x,y:A*//(x R y))) (x,y,z:A*. (x R y) ((z @ x) R (z @ y))) (g:((x,y:A*//(x R y))). l:A*. L(l) g(l)) (m:. m ~ (x,y:A*//(x L-induced Equiv y))) & (l:A*. Dec(L(l))) mn_23

Thm* n:. nn+1 nxn_plus_1_ge_0

Thm* P:(Prop), n:. (k:{n...}. P(k) (i:k. P(i))) & (m:. P(m)) (m:n. P(m)) mn_23_lem_0

In prior sections: int 1 bool 1 int 2 list 1 finite sets list 3 autom exponent languages action sets det automata