∀[A:Type]. ∀[as:A List]. ∀[i:ℤ].  (nth_tl(i;as) ∈ A List)
{ (UnivCD THENA Auto) }
1. A : Type
2. as : A List
3. i : ℤ
⊢ nth_tl(i;as) ∈ A List