How to define init for vectors?

I try to write small familiar programs to understand dependent types
programming better (more precisely, understand it at all). All usual
maps and folds are done and I processed to more dependent ones.

That's what I managed to write:
------------------------------------------------------------------------------
                                          (   n : Nat    !
data (---------!  where (------------! ;  !--------------!
     ! Nat : * )        ! zero : Nat )    ! succ n : Nat )
------------------------------------------------------------------------------
     (    A : *    !                                 (      a : A       !
data !-------------!  where (-------------------! ;  !------------------!
     ! Maybe A : * )        ! Nothing : Maybe A )    ! Just a : Maybe A )
------------------------------------------------------------------------------
     ( A : * ;  B : * !        (    a : A ;  b : B    !
data !----------------!  where !----------------------!
     !  Pair A B : *  )        ! Tuple a b : Pair A B )
------------------------------------------------------------------------------
     ( n : Nat ;  X : * !                            ( x : X ;  xs : Vec n X !
data !------------------!  where (--------------! ;  !-----------------------!
     !   Vec n X : *    )        ! vnil :       !    !   vcons x xs :        !
                                 !   Vec zero X )    !     Vec (succ n) X    )
------------------------------------------------------------------------------
let  (-------------!
     ! width : Nat )

     width => succ (succ zero)
------------------------------------------------------------------------------

And here I got stuck:
------------------------------------------------------------------------------
     ( X : * ;  xs : Vec (succ n) X !
let  !------------------------------!
     !     vecInit xs : Vec n X     )

     vecInit xs <= case xs
       { vecInit (vcons n' ns) => vcons n' (vecInit ns)
       }
------------------------------------------------------------------------------
This is a version of init function from Haskell Prelude:
init [x] = []
init (x:xs) = x:init xs
I do not get second case from Epigram when elaborating. And, actually,
Epigram does not like "=> vcons n' (vecInit ns)" part. But I can
understand that, albeit not formally.

Where should I look for hints on to get a clue on how to do it right?