structure ListTag =
    struct
	assert sub <| {i:nat, size:nat | i < size} 'a array(size) * int(i) -> 'a
        assert nth <| {i:nat, size:nat | i < size} 'a list(size) *  int(i) -> 'a

	fun{times:nat} test(arr, times) =
	    let
		val l = [1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16]
		fun aux(n) =
		    if n = times then ()
		    else (nth(l, sub(arr, n) mod 16); aux(n+1))
                where aux <| {n:nat | n <= times} int(n) -> unit
	    in
		aux(0)
	    end
        where test <| {size:nat | times <= size}
                         int array(size)  * int(times) -> unit
    end