U11(tt) → U12(splitAt(N, XS))
U12(pair(YS, ZS)) → pair(cons(X), ZS)
and(tt) → X
tail(cons(N)) → XS
afterNth(N, XS) → snd(splitAt(N, XS))
fst(pair(X, Y)) → X
head(cons(N)) → N
natsFrom(N) → cons(N)
sel(N, XS) → head(afterNth(N, XS))
snd(pair(X, Y)) → Y
splitAt(0, XS) → pair(nil, XS)
splitAt(s(N), cons(X)) → U11(tt)
take(N, XS) → fst(splitAt(N, XS))