1. n : {1...}

2. A :

3. L : L(A)

4. L A List

5. R : A List A List

6. Fin(A)

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

8. 1-1-Corresp(n;x,y:(A List)//(x R y))

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

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

11. l:A List. L l (g l)

12. l : A List

Dec(L l)

None