Level: Lib Thy Top: 1
Hypotheses:

  1. Alph :

  2. M : L(Alph)

Conclusion:

(M) L(Alph)

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

None