None

Conclusion:

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

1. x Rl y x Rg y

2. L A List