1. A :

2. R : A List A List

3. EquivRel(A List;x,y.x R y)

4. x,y,z:A List. x R y (z @ x) R (z @ y)

5. g : x,y:(A List)//(x R y)

6. a : x,y:(A List)//(x R y)

7. b : x,y:(A List)//(x R y)

8. z:A List. (g z@a) (g z@b)

9. z : A List

10. (g z@b)

(g z@a)

None