Level:
Lib
Thy
Top
:
Hypotheses:
None
Conclusion:
Alph:
.
L,L':L(Alph).
n,n':
. L = L'
n = n'
(L
n) = (L'
n')
Applied Tactic:
UnivCD THENW Auto
Generated subgoals:
1
. (L
n) = (L'
n')
Alph:
. L,L':L(Alph). n,n':
. L = L' 
n = n' (L
n) = (L'n')n) = (L'n')