Finite list induction principle and the tail eliminator
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