Level:
Lib
Thy
Top
:
Hypotheses:
None
Conclusion:
Alph:
.
L,L':L(Alph). L = L'
(L
) = (L'
)
Applied Tactic:
Unfold `lang_closure` 0 THEN UnivCD THENW Auto
Generated subgoals:
1
.
l.
n:
. (L
n) l =
l.
n:
. (L'
n) l
Alph:
. L,L':L(Alph). L = L' 
(L
) = (L')
l.
n:
. (Ln) l = l.n:. (L'n) l