Level:
Lib
Thy
Top
:
1
Hypotheses:
Alph :
L : L(Alph)
L' : L(Alph)
L = L'
Conclusion:
l.
n:
. (L
n) l =
l.
n:
. (L'
n) l
Applied Tactic:
Unfold `lang_eq` 0
Generated subgoals:
1
.
l:Alph List. (
l.
n:
. (L
n) l) l
(
l.
n:
. (L'
n) l) l
l.
n:
. (L
n) l = l.n:. (L'n) l
l:Alph List. (l.n:. (Ln) l) l 
(l.n:. (L'n) l) l