Thm* R:(Alph*Alph*Prop). (EquivRel x,y:Alph*. x R y) (x,y,z:Alph*. (x R y) ((z @ x) R (z @ y))) (z1,z2:Alph*, y:x,y:Alph*//(x R y). z1 @ z2@y = z1@z2@y) mn_quo_append_assoc