Finite list induction principle and the tail eliminator

Question

In Dybjer's Inductive Families the author present a method to derive an eliminator/induction principle for every inductive family of types.

In particular for the type of finite lists, namely $$List' \colon (A \colon set) (n \colon N) set$$ we get the eliminator $$\begin{align*} listrec' \colon &(A \colon set)\\ & (C \colon (a \colon N)(c \colon List'_A n)set) \\ & (e_1 \colon C(0,nil'_A)\\ & (e_2 \colon (b_1 \colon N)(b_2 \colon A)(u \colon List'_A(b_1))(v \colon C(b_1,u))C(s(b_1),cons'_A(b_1,b_2,u)))\\ & (a \colon N) \\ & (c \colon List'_A(a)) \\ & C(a,c)\ . \end{align*}$$

From what I get from this eliminator we should be able to provide any possible operation using finite lists.

Now my question is

how do we get the classical destructor $$tail \colon (A \colon set)(n \colon N)(List'_A(s(n))) List'_A n$$ that from any finite list gets its tail?

I am totally lost on how to approach this problem since the eliminator seems to be able to provide just function defined on the whole family $List'_A(n)$ and not on the sub-family $List'_A(s(n))$.

Thanks in advance.