PrintForm Definitions languages Sections AutomataTheory Doc

At: lang eq weakening


Alph:Type, L,M:LangOver(Alph). L = M L = M

By: UnivCD

Generated subgoal:

11. Alph: Type
2. L: LangOver(Alph)
3. M: LangOver(Alph)
4. L = M
L = M


About:
alluniverseimpliesequal