None

Conclusion:

Alph:. L:L(Alph). R:Alph List Alph List . EquivRel(Alph List;x,y.x R y) (g:x,y:(Alph List)//(x R y) . l:Alph List. L l (g l)) (x,y,z:Alph List. x R y (z @ x) R (z @ y)) (x,y:Alph List. x R y x Rl y)

1. x Rl y

2. L Alph List