Level: Lib Thy Top:
Hypotheses:None
Conclusion:
Alph:
. R:Alph List 
Alph List 
.
EquivRel(Alph List;x,y.x R y)
(x,y,z:Alph List. x R y (z @ x) R (z @ y))
(z1,z2:Alph List. y:x,y:(Alph List)//(x R y). z1 @ z2@
y = z1@z2@y)
Applied Tactic: UnivCD THENW Auto
Generated subgoals:1. z1 @ z2@y = z1@z2@y