PrintForm Definitions languages Sections AutomataTheory Doc

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

M = L
By:
Unfold `lang_eq` 0
THEN
Unfold `lang_eq` 4
Generated subgoal:

14. l:Alph*. L(l) M(l)
l:Alph*. M(l) L(l)

About:
universealllistapply