f:(nSt). Bij(n; St; f)

(l:Alph*. LangOf(Auto)(l)) (k:(n+1), l:{l:(Alph*)| ||l|| = k }. LangOf(Auto)(l))

Dec(k:(n+1), l:{l:(Alph*)| ||l|| = k }. LangOf(Auto)(l))

Inst Thm* R:(TProp). Fin(T) & (t:T. Dec(R(t))) Dec(t:T. R(t)) [(n+1);k.l:{l:(Alph*)| ||l|| = k }. LangOf(Auto)(l)]
THEN
Try (Fold `languages` 0)

1	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)) Fin((n+1))
2	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) Dec((k.l:{l:(Alph*)| ||l|| = k }. LangOf(Auto)(l))(t))
3	8. Dec(t:(n+1). (k.l:{l:(Alph*)| ||l|| = k }. LangOf(Auto)(l))(t)) Dec(k:(n+1), l:{l:(Alph*)| ||l|| = k }. LangOf(Auto)(l))

About: