PrintForm Definitions languages Sections AutomataTheory Doc

At: lang eq inversion 1 1 1 1
1. Alph: Type
2. L: LangOver(Alph)
3. M: LangOver(Alph)
4. l: Alph*
5. L(l) M(l)

M(l) L(l)
By:
Unfold `languages` 2
THEN
Unfold `languages` 3
THEN
RWH (HypC 5) 0
Generated subgoals:

None

About:
applyuniverselist