PrintForm Definitions myhill nerode Sections AutomataTheory Doc

At: mn quo append assoc 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
By: RWH (UnfoldC `mn_quo_append`) 0
Generated subgoal:

1 ((z1 @ z2) @ y) = (z1 @ z2 @ y) x,y:Alph*//(x R y)

About:
equalquotientlistuniversefunctionpropallimplies