PrintForm Definitions languages Sections AutomataTheory Doc

At: lang union inters

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

11. Alph: Type
2. L: Alph*Prop
3. M: Alph*Prop
4. N: Alph*Prop
5. l: Alph*
(l.L(l) (l.M(l) & N(l))(l))(l) (l.(l.L(l) M(l))(l) & (l.L(l) N(l))(l))(l)

About:
alluniverseapplylambdaorand