PrintForm Definitions myhill nerode Sections AutomataTheory Doc

At: mn quo append assoc 1 1
1. Alph: Type
2. R: Alph*Alph*Prop
3. EquivRel x,y:Alph*. x R y
4. x,y,z:Alph*. (x R y) ((z @ x) R (z @ y))
5. z1: Alph*
6. z2: Alph*
7. y: x,y:Alph*//(x R y)

((z1 @ z2) @ y) = (z1 @ z2 @ y) x,y:Alph*//(x R y)
By: Analyze 7
Generated subgoal:

17. y1: Alph*
8. y2: Alph*
9. y1 R y2
((z1 @ z2) @ y1) = (z1 @ z2 @ y2) x,y:Alph*//(x R y)

About:
equalquotientlistuniversefunctionpropallimplies