PrintForm Definitions myhill nerode Sections AutomataTheory Doc

At: lang rel equi

A:Type, L:LangOver(A). EquivRel x,y:A*. x L-induced Equiv y
By:
UnivCD
THEN
Unfold `equiv_rel` 0
Generated subgoal:

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

About:
alluniverselistand