Level: Lib Thy Top: 1
Hypotheses:

  1. Alph :

  2. L : L(Alph)

  3. L' : L(Alph)

  4. n :

  5. n' :

  6. L = L'

  7. n = n'

Conclusion:

(Ln) = (L'n')


Applied Tactic: RWH (RevHypC 7) 0 THENA Auto
Generated subgoals:

1. (Ln) = (L'n)