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