(type_abbrev 'int = exists 'i:I (S('i)) in

(type_abbrev 'tone = 
 (exists 'bp:L(1,1)((mu('bp<-{'b}){'a}(unit + ('b * 'a))) * 
                    (mu('bp<-{'b}){'a}(unit + ('a * (('b * 'int)->'int)))))) in

(let zero  : 'int = pack 0,0 as 'int in
(let one   : 'int = pack 1,1 as 'int in
(let two   : 'int = pack 2,2 as 'int in
(let three : 'int = pack 3,3 as 'int in
(let four  : 'int = pack 4,4 as 'int in

(let apply_nth : 'tone -> 'int -> 'int = 
  (fun x : 'tone . (fun n : 'int .
    (let f : 'tone -> 'int -> 'int =
     (fix (fun f : 'tone -> 'int -> 'int . (fun x : 'tone . (fun n : 'int .
      (unpack x as 'bp,x in
      (peel x as {'aone,'atwo},xtwo in
      (case (unroll (xtwo.1))
       xthree. zero
       xthree. 
        (case (unroll (xtwo.2))
         xfour. zero
         xfour. 
          (unpack n as 'ntyp,ntwo in
          (ifE (1),(ntwo)
           then ((xfour.2) ((xthree.1), zero))
           else ((f (pack 'atwo,((xthree.2),(xfour.1)) as 'tone)) 
                    (decr n))))))))))))
     in
    ((f x) n))))
in 

(let cons : 'tone -> (exists 'a:T ('a * (('a * 'int)->'int))) -> 'tone =
 (fun x : 'tone . (fun c : (exists 'a:T ('a * (('a * 'int)->'int))) .
  (unpack x as 'bp,xtwo in
  (unpack c as 'ap,ctwo in
  (pack ({'ap}::(1,1){'bp}),
    ((roll (in2 ((ctwo.1),(xtwo.1)) unit) as 
      (mu(({'ap}::(1,1){'bp})<-{'b}){'a} (unit + ('b * 'a)))),
     (roll (in2 ((xtwo.2),(ctwo.2)) unit) as
      (mu(({'ap}::(1,1){'bp})<-{'b}){'a} (unit + ('a * (('b * 'int)->'int))))))
   as 'tone))))) 
in

(let empty_list : 'tone =
 (pack ({unit}::(1,1){({unit}!(1))}),
   ((roll (in1 () (unit * (mu(({unit}!(1))<-{'b}){'a} (unit + ('b * 'a))))) as
      (mu(({unit}::(1,1){({unit}!(1))})<-{'b}){'a} (unit + ('b * 'a)))),
    (roll (in1 () ((mu(({unit}!(1))<-{'b}){'a} 
                      (unit + ('a * (('b * 'int)->'int)))) * 
                   ((unit * 'int)->'int))) as
      (mu(({unit}::(1,1){({unit}!(1))})<-{'b}){'a}
         (unit + ('a * (('b * 'int)->'int))))))
  as 'tone) 
in

(let list : 'tone = 
 ((cons ((cons 
    (empty_list)) 
    (pack 'int,(three, (fun x : ('int * 'int) . (x.1))) as
      (exists 'a:T ('a * (('a * 'int)->'int))))))
    (pack 'int,(four, (fun x : ('int * 'int) . (incr x.2))) as
      (exists 'a:T ('a * (('a * 'int)->'int)))))
    
in
 
(((apply_nth list) one),(((apply_nth list) two),((apply_nth list) three))))))))))))))