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 &amp;(A \colon set)\\
&amp; (C \colon (a \colon N)(c \colon List'_A n)set) \\
&amp; (e_1 \colon C(0,nil'_A)\\
&amp; (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)))\\
&amp; (a \colon N) \\
&amp; (c \colon List'_A(a)) \\
&amp; 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) -&gt; n = s(m) -&gt; 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)) -&gt; C(n, xs)
gtail A = listrec' A C
          contradiction -- of type: (m:N) -&gt; 0 = s(m) -&gt; List'_A(m)
          (\ _ _ u _ -&gt; u)

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