Level: Lib Thy Top: 1
Hypotheses:

  1. Alph :

Conclusion:

L(Alph) '

Applied Tactic: Unfold `languages` 0 THEN Auto
Generated subgoals:

None