 
  g:((x,y:Alph*//(x L-induced Equiv y))
g:((x,y:Alph*//(x L-induced Equiv y))

 ). (
). ( l:Alph*. L(l)
l:Alph*. L(l) 
 g(l))
 g(l)) 
 LangOf(A(g)) = L
 LangOf(A(g)) = L L:LangOver(A). EquivRel x,y:A*. x L-induced Equiv y
[Alph;L]
L:LangOver(A). EquivRel x,y:A*. x L-induced Equiv y
[Alph;L]| 1 | 3. EquivRel x,y:Alph*. x L-induced Equiv y    g:((x,y:Alph*//(x L-induced Equiv y))    ). (  l:Alph*. L(l)   g(l))   LangOf(A(g)) = L | 
About:
|  |  |  |  |  | 
|  |  |  |  |