(0) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

from(X) → cons(X, from(s(X)))
sel(0, cons(X, Y)) → X
sel(s(X), cons(Y, Z)) → sel(X, Z)

Q is empty.