Finite list induction principle and the tail eliminator

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.

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)).

The typical trick in this situation is to pick a C such that you can pretend you are defining a function on the whole family when, in fact, you're only focusing on the sub-family you care about thanks to equality constraints.

Let me be more concrete:

If you pick C(n, xs) = (m:N) -> n = s(m) -> List'_A(m) then you can define a generalised gtail by using listrec', and derive tail as a corollary.

gtail : (A:set) (n:N) (xs : List'_A(n)) -> C(n, xs)
gtail A = listrec' A C
          contradiction -- of type: (m:N) -> 0 = s(m) -> List'_A(m)
          (\ _ _ u _ -> u)

tail : (A:set) (n:N) -> List′A (s(n)) -> List′An
tail A n xs = gtailn A (s(n)) xs n refl

StackExchange Computer Science Q#96557, answer score: 3