N : Set 0;
O : N;
S : N -> N;

one   : N = S O;
two   : N = S (S O);
three : N = S two;

data Vect : (A:Set 0) -> (n:N) -> Set 0 where
    Nil  : (A:Set 0) -> (Vect A O)
  | Cons : (A:Set 0) -> (k:N) -> (a:A) -> (Vect A k) -> (Vect A (S k));

vtail : (A:Set 0) -> (k:N) -> (Vect A (S k)) -> (Vect A k);