------------------------------------------------------------------------------
                                  (   x : Nat    !
data Nat : *  where zero : Nat ;  !--------------!
                                  ! succ x : Nat )
------------------------------------------------------------------------------
     ( l : Nat ;  t : * !                                              
data !------------------!                                              
     !   Vec l t : *    )                                              
                                                                       
                          ( l : Nat ;  t : * ;  v : t ;  vs : Vec l t !
where (--------------! ;  !-------------------------------------------!
      ! vempty t :   !    !      vcons l t v vs : Vec (succ l) t      )
      !   Vec zero t )                                                 
------------------------------------------------------------------------------
     ( x : Nat ;  y : Nat !              
let  !--------------------!              
     !   add x y : Nat    )              
                                         
     add x y <= case x                   
     { add zero y => y                   
       add (succ x) y <= rec x           
       { add (succ x) y => add x (succ y)
       }                                 
     }                                   
------------------------------------------------------------------------------
     ( l1 : Nat ;  l2 : Nat ;  t : * ;  vs1 : Vec l1 t ;  vs2 : Vec l2 t !
let  !-------------------------------------------------------------------!
     !            vappend l1 l2 t vs1 vs2 : Vec (add l1 l2) t            )
                                                                          
     vappend l1 l2 t vs1 vs2 <= case vs1                                  
     { vappend zero l2 t (vempty t) vs2 => vs2                            
       vappend (succ l) l2 t (vcons l t v vs) vs2                         
         => vcons (add l l2) t v (vappend l l2 t vs vs2)                  
     }                                                                    
------------------------------------------------------------------------------