At: mn quo append assoc 1 1 1 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. y1: Alph*
8. y2: Alph*
9. y1 R y2
((z1 @ z2) @ y1) R ((z1 @ z2) @ y2)
By: BackThru 4
Generated subgoals:None
About:
