Level: Lib Thy Top:
Hypotheses:

None

Conclusion:

Alph:. L,L',M,M':L(Alph). L = L' M = M' (L M) = (L' M')

Applied Tactic: Unfold `languages` 0 THEN Unfold `lang_eq` 0 THEN Unfold `lang_inters` 0 THEN UnivCD THENW Auto
Generated subgoals:

1. (l.L l M l) l (l.L' l M' l) l