Level:
Lib
Thy
Top
:
1
Hypotheses:
Alph :
L : L(Alph)
L' : L(Alph)
n :
n' :
L = L'
n = n'
Conclusion:
(L
n) = (L'
n')
Applied Tactic:
RWH (RevHypC 7) 0 THENA Auto
Generated subgoals:
1
. (L
n) = (L'
n)