At: empty lang dec 1 1 1 2 1 2 1 3 1
1. Alph: Type
2. St: Type
3. Auto: Automata(Alph;St)
4. Fin(Alph)
5. n: 
6. 
f:(n
St). Bij(n; St; f)
7. (l:Alph*. LangOf(Auto)(l)) 
(k:(n+1), l:{l:(Alph*)| ||l|| = k }. LangOf(Auto)(l))
8. (l:Alph*. LangOf(Auto)(l)) 
(k:(n+1), l:{l:(Alph*)| ||l|| = k }. LangOf(Auto)(l))
9. t: (n+1)
10. t1: {l:(Alph*)| ||l|| = t }
Dec(LangOf(Auto)(t1))
By:
Unfold `auto_lang` 0
THEN
Reduce 0
THEN
ProveDecidable
Generated subgoals:None
About:
