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