Level: Lib Thy Top: 1
Hypotheses:

  1. Alph :

  2. M : L(Alph)

  3. N : L(Alph)

Conclusion:

(M U N) L(Alph)

Applied Tactic: Unfold `lang_union` 0
Generated subgoals:

1. (l.M l N l) L(Alph)