PrintForm Definitions languages Sections AutomataTheory Doc

At: lang inters functionality

Alph:Type, L,L',M,M':LangOver(Alph). L = L' M = M' (L M) = (L' M')
By:
Unfold `languages` 0
THEN
Unfold `lang_eq` 0
THEN
Unfold `lang_inters` 0
THEN
UnivCD
Generated subgoal:

11. Alph: Type
2. L: Alph*Prop
3. L': Alph*Prop
4. M: Alph*Prop
5. M': Alph*Prop
6. l:Alph*. L(l) L'(l)
7. l:Alph*. M(l) M'(l)
8. l: Alph*
(l.L(l) & M(l))(l) (l.L'(l) & M'(l))(l)

About:
alluniverseimpliesapplylambdaand