PrintForm Definitions myhill nerode Sections AutomataTheory Doc

At: lang rel refl 1
1. A: Type
2. L: LangOver(A)

Refl(A*;x,y.x L-induced Equiv y)
By:
Unfolds [`refl`;`lang_rel`] 0
THEN
Reduce 0
Generated subgoal:

1 a,z:A*. L(z @ a) L(z @ a)

About:
listuniverseallapply