PrintForm Definitions myhill nerode Sections AutomataTheory Doc

At: mn 23 refinment 2
1. Alph: Type
2. L: LangOver(Alph)
3. R: Alph*Alph*Prop
4. EquivRel x,y:Alph*. x R y
5. g: (x,y:Alph*//(x R y))
6. l: Alph*

L Alph*Prop
By: Unfold `languages` 2
Generated subgoals:

None

About:
memberfunctionlistpropuniversequotientbool