PrintForm Definitions languages Sections AutomataTheory Doc

At: lang eq inversion 1 1 1

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

M(l) L(l)

By: Witness4 l

Generated subgoal:

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


About:
applyuniversealllist