PrintForm Definitions languages Sections AutomataTheory Doc

At: lang eq transitivity

Alph:Type, L,M,N:LangOver(Alph). L = M M = N L = N
By:
Unfold `languages` 0
THEN
Unfold `lang_eq` 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) M(l)
6. l:Alph*. M(l) N(l)
7. l: Alph*
L(l) N(l)

About:
alluniverseimpliesapply