At: lang power functionality 1 1 1 2 1 1 1 2 4
1. Alph: Type
2. L: LangOver(Alph)
3. L': LangOver(Alph)
4. n': 
5. L = L'
6. n: 
7. 0 < n
8. (L
n-1) = (L'n-1)
9. l: Alph*
10. 
n = 0
((L'n-1)
L') 
Alph*
Prop
By: Fold `languages` 0
Generated subgoals:None
About:
