DML , ML with restricted dependent types

Question

Refering to this paper Dependent ML: An Approach to Practical Programming with Dependent Types

Have defined datatype 'alist ( int ) Its not clear why they have used int as a parameter rather than a nat directly.

datatype ’a list (int) = 
    nil(0) | {n:nat} cons(n+1) of ’a * ’a list(n)
fun(’a)
    append (nil, ys) = ys
  | append (cons (x, xs), ys) = cons (x, append (xs, ys))
withtype {m:nat,n:nat} ’a list(m) * ’a list(n) -> ’a list(m+n)

In there base paper Dependent Types in Practical Programming they have defines it like ’a list of nat which makes more sense :

datatype ’a list = nil | cons of ’a * ’a list
typeref ’a list of nat with (* indexing the datatype ’a list with nat *)
    nil <| ’a list(0)
  | cons <| {n:nat} ’a * ’a list(n) -> ’a list(n+1)

fun(’a)
    append(nil, ys) = ys 
  | append(cons(x, xs), ys) = cons(x, append(xs, ys))
where append <| {m:nat}{n:nat} ’a list(m) * ’a list(n) -> ’a list(m+n)

The first declaration looks elegant and In second its not clear why to use <| inside where clause ? Can anyone help me with this.