(datatype seq

  ____________
  [] : (seq 0 A);
  
  X : A; Y : (seq N A);
  =================
  [X | Y] : (seq (+ 1 N) A);)

(define tlseq
  {(seq (+ 1 N) A) --> (seq N A)}
  [_ | Y] -> Y)