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

Thm* q:, E:(q*q*Prop). (EquivRel x,y:q*. x E y) & (x,y:q*. Dec(x E y)) (h:(q*q*). (x,y:q*. (x E y) h(x) = h(y)) & (x:q*. x E (h(x)))) list_quo_choice

Thm* q:, x:q*. q = 0 x = nil empty_alph_list

Thm* q:, E:(q*q*Prop). (EquivRel x,y:q*. x E y) & (x,y:q*. Dec(x E y)) (h:(q*q*). (x,y:q*. (x E y) h(x) = h(y)) & (x:q*. x E (h(x)))) list_quo_choice_pls

In prior sections: int 1 bool 1 choice 1 int 2 list 1 finite sets list 3 autom exponent relation autom det automata myhill nerode