E:(Alph*
Alph*Prop).
Fin(Alph) & (EquivRel x,y:Alph*. x E y) & (x,y:Alph*. Dec(x E y)) 
(
h:(Alph*Alph*).
(x,y:Alph*. (x E y) 
h(x) = h(y)) & (x:Alph*. x E (h(x))))
fin_alph_list_quo
Thm* E:(Alph*Alph*Prop).
Fin(Alph) & (EquivRel x,y:Alph*. x E y) & (x,y:Alph*. Dec(x E y))
(h:(Alph*Alph*).
(x,y:Alph*. (x E y) h(x) = h(y)) & (x:Alph*. x E (h(x))))
fin_alph_list_quo
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:
, 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: rel 1 choice 1 quot 1 relation autom myhill nerode