At: lang power functionality 1 1 1 2 1 1 1 2 6
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)(l) 
((L'n-1)L')(l)
By:
RWH (HypC 5) 0
THEN
Fold `languages` 0
Generated subgoals:None
About:
