PrintForm Definitions myhill nerode Sections AutomataTheory Doc

At: lang rel symm

A:Type, L:LangOver(A). Sym x,y:A*. x L-induced Equiv y
By: UnivCD
Generated subgoal:

11. A: Type
2. L: LangOver(A)
Sym x,y:A*. x L-induced Equiv y

About:
alluniverselist