PrintForm
Definitions
myhill
nerode
Sections
AutomataTheory
Doc
At:
fin
listify
1
1.
T:
Type
2.
Fin(T)
TL:T*.
t:T. mem_f(T;t;TL)
By:
Analyze -1
THEN
Analyze -1
Generated subgoal:
1
2.
n:
3.
f:
n
T
4.
Bij(
n; T; f)
TL:T*.
t:T. mem_f(T;t;TL)
About:
n
Tn; T; f)
TL:T*. 
t:T. mem_f(T;t;TL) TL:T*. t:T. mem_f(T;t;TL)nTn; T; f) TL:T*. t:T. mem_f(T;t;TL)
