(type_abbrev 'int   = exists 'i:I (S('i)) in
(type_abbrev 'color = 'int in
(type_abbrev 'bool  = S(0) + S(1) in
(let false:'bool = in1 0 S(1) in
(let true :'bool = in2 1 S(0) in
(let blacku :S(0) = 0 in
(let redu   :S(1) = 1 in 
(let blackp : 'int = (pack 0,blacku as 'color) in
(let redp   : 'int = (pack 1,redu as 'color) in

(type_abbrev 'coordTrInt = 
  exists 'rblst:L(1,2)
    ((mu('rblst<-{'b}){'aone,'atwo} 
    	('b*(if 'b then unit else ('int * ('aone * 'atwo)))))
     * (mu('rblst<-{'b}){'aone,'atwo} 
        (if 'b then S(0) else ('color * ('aone * 'atwo)))))
in
(type_abbrev 'valTrInt =
  exists 'rblst:L(1,2)
     (mu('rblst<-{'b}){'aone,'atwo} 
        ('b*(if 'b then unit else ('int * ('aone*'atwo)))))
in

(let emptytree : 'coordTrInt =
  (type_abbrev 'empty_sigma = {S(1)}::(1,2){({S(1)}!(2)),({S(1)}!(2))} in
  (type_abbrev 'nil_val_branch = mu(({S(1)}!(2))<-{'b}){'aone,'atwo} 
                                  ('b*(if 'b then unit 
                                       else ('int * ('aone*'atwo)))) in
  (type_abbrev 'nil_color_branch = mu(({S(1)}!(2))<-{'b}){'aone,'atwo} 
                                     (if 'b then S(0)
                                      else ('color * ('aone * 'atwo))) in
  pack 'empty_sigma,
  (
   (roll (1,(tosum (()),(if S(1) then unit 
                         else ('int * ('nil_val_branch * 'nil_val_branch)))))
    as (mu('empty_sigma<-{'b}){'aone,'atwo} 
       ('b*(if 'b then unit else ('int *('aone*'atwo))))))
   ,  
   (roll (tosum (0),(if S(1) then S(0) 
                     else ('color * ('nil_color_branch * 'nil_color_branch))))
    as (mu('empty_sigma<-{'b}){'aone,'atwo} 
       (if 'b then S(0) else ('color*('aone*'atwo))))))
  
 as 'coordTrInt)))
in 

(let lookup : 'int -> 'coordTrInt -> 'bool =
  (fun key : 'int.
   (fun tree : 'coordTrInt .
     (unpack key as 'sktyp,searchk in
       ((fix (fun lookup: 'valTrInt -> 'bool .
                  (fun tree:'valTrInt .
                       (unpack tree as 'trlsttyp,tr in
                         (peel (tr,tr) as {'ahd,'atla,'atlb},ptr in
                           (match (unroll (ptr.1))
                            uptr.
                              false
                            uptr.
                              (unpack (uptr.1) as 'trktyp,treek in
                                (ifE (searchk),(treek)
                                 then true
                                 else 
                                   (ifG (searchk),(treek)
                                    then
                                      (lookup
	                                (pack 'atlb,((uptr.2).2) as 'valTrInt))
                                    else
                                      (lookup  
                                       (pack 'atla,((uptr.2).1) as 'valTrInt))))
	)))))))
         (unpack tree as 'trlsttyp,tr in
              (pack 'trlsttyp,tr.1 as 'valTrInt))))))
in 

(let insert : 'int -> 'coordTrInt -> 'coordTrInt =
   (type_abbrev 'valTrBody  = 'b*(if 'b then unit else ('int*('aone*'atwo))) in
   (type_abbrev 'leftValTr  = mu('sigmaL<-{'b}){'aone,'atwo} 'valTrBody in
   (type_abbrev 'rightValTr = mu('sigmaR<-{'b}){'aone,'atwo} 'valTrBody in
   (type_abbrev 'colTrBody  = if ('b) then (S(0)) else ('color*('aone*'atwo)) in
   (type_abbrev 'leftColTr  = mu('sigmaL<-{'b}){'aone,'atwo} 'colTrBody in
   (type_abbrev 'rightColTr = mu('sigmaR<-{'b}){'aone,'atwo} 'colTrBody in
   (let mkTree : all 'sigmaL:L(1,2) (all 'sigmaR:L(1,2) 
                  ('int -> 'color -> 
	           'leftValTr -> 'rightValTr -> 'leftColTr -> 'rightColTr
                   -> 'coordTrInt)) =
      (fun 'sigmaL:L(1,2). (fun 'sigmaR:L(1,2) .
      (fun key:'int. (fun color:'color .
      (fun leftVal:'leftValTr. (fun rightVal:'rightValTr.
      (fun leftCol:'leftColTr. (fun rightCol:'rightColTr.
         (pack ({S(0)}::(1,2){'sigmaL,'sigmaR}),
             (
               (roll (0,(tosum (key, (leftVal, rightVal)),
                               (if S(0) then unit
                                else ('int * ('leftValTr * 'rightValTr)))))
                as  (mu(({S(0)}::(1,2){'sigmaL,'sigmaR})<-{'b}){'aone,'atwo}
                      'valTrBody)),
               (roll (tosum (color, (leftCol, rightCol)),
                               (if S(0) then S(0)
                                else ('color * ('leftColTr * 'rightColTr))))
                as  (mu(({S(0)}::(1,2){'sigmaL,'sigmaR})<-{'b}){'aone,'atwo}
                      'colTrBody)))
           as 'coordTrInt))))))))) in

   (let setleftc : 'coordTrInt -> 'coordTrInt -> 'coordTrInt =
       (fun tree : 'coordTrInt. (fun newleft : 'coordTrInt .
           (unpack tree as 'trlsttyp, unptree in
           (unpack newleft as 'newltyp,unpnewl in
           (peel unptree as {'ahd,'atla,'atlb},pltree in
           (match (unroll (pltree.1))
             mtreeone. tree
             mtreeone.
               (match ((unroll (pltree.1)).1,(unroll (pltree.2)))
                 mtreetwo. tree
                 mtreetwo. ((((((((mkTree ['newltyp]) ['atlb])
	                   	   mtreeone.1) mtreetwo.1)
	                           unpnewl.1) (mtreeone.2).2)
                                   unpnewl.2) (mtreetwo.2).2)))))))) in
    (let setrightc : 'coordTrInt -> 'coordTrInt -> 'coordTrInt =
       (fun tree : 'coordTrInt. (fun newright : 'coordTrInt .
           (unpack tree as 'trlsttyp, unptree in
           (unpack newright as 'newrtyp,unpnewr in
           (peel unptree as {'ahd,'atla,'atlb},pltree in
           (match (unroll (pltree.1))
             mtreeone. tree
             mtreeone.
               (match ((unroll (pltree.1)).1,(unroll (pltree.2)))
                 mtreetwo. tree
                 mtreetwo. ((((((((mkTree ['atla]) ['newrtyp])
	                   	   mtreeone.1) mtreetwo.1)
                                   (mtreeone.2).1) unpnewr.1)
                                   (mtreetwo.2).1) unpnewr.2)))))))) in
    (let leftchild : 'coordTrInt -> 'coordTrInt =
        (fun tree : 'coordTrInt .
           (unpack tree as 'trtyp,unptree in
           (peel unptree as {'ahd,'atla,'atlb},pltree in
           (match (unroll (pltree.1))
              mtreeone. tree
              mtreeone.
                (match ((unroll (pltree.1)).1,(unroll (pltree.2)))
                 mtreetwo. tree
                 mtreetwo.
                  (pack 'atla,((mtreeone.2).1,(mtreetwo.2).1) 
                   as 'coordTrInt)))))) in
    (let rightchild : 'coordTrInt -> 'coordTrInt =
        (fun tree : 'coordTrInt .
           (unpack tree as 'trtyp,unptree in
           (peel unptree as {'ahd,'atla,'atlb},pltree in
           (match (unroll (pltree.1))
              mtreeone. tree
              mtreeone.
                (match ((unroll (pltree.1)).1,(unroll (pltree.2)))
                 mtreetwo. tree
                 mtreetwo.
                  (pack 'atlb,((mtreeone.2).2,(mtreetwo.2).2) 
                   as 'coordTrInt)))))) in
    (let setcolor : 'coordTrInt -> 'color -> 'coordTrInt =
         (fun tree  : 'coordTrInt .
         (fun color : 'color .
            (unpack tree as 'trlsttyp, unptree in
            (peel unptree as {'ahd,'sigmaL,'sigmaR},pltree in
            (match (unroll (pltree.1))
             mtreeone. tree
             mtreeone.
               (match ((unroll (pltree.1)).1,(unroll (pltree.2)))
                 mtreetwo. tree
                 mtreetwo.
	         (pack ({S(0)}::(1,2){'sigmaL,'sigmaR}),
                   (
                     (roll (0,(tosum mtreeone,
                               (if S(0) then unit
                                else ('int * ('leftValTr * 'rightValTr)))))
                    as  (mu(({S(0)}::(1,2){'sigmaL,'sigmaR})<-{'b}){'aone,'atwo}
                          'valTrBody)),
                     (roll (tosum (color, mtreetwo.2),
                               (if S(0) then S(0)
                                else ('color * ('leftColTr * 'rightColTr))))
                    as  (mu(({S(0)}::(1,2){'sigmaL,'sigmaR})<-{'b}){'aone,'atwo}
                          'colTrBody)))
                  as 'coordTrInt))))))) in
     (let isblack : 'coordTrInt -> 'bool =
	(fun tree : 'coordTrInt.
           (unpack tree as 'trlsttyp,unptree in
           (peel unptree as {'ahd,'atla,'atlb},pltree in
              (match ((unroll (pltree.1)).1,(unroll (pltree.2)))
                    mtree. true
                    mtree. 
                      (unpack (mtree.1) as 'cltyp,color in
                        (ifE color,blacku
                         then true
                         else false)))))) in 
     (let isred : 'coordTrInt -> 'bool =
	(fun tree : 'coordTrInt. 
           (case (isblack tree) x. true x. false)) in
     (let balance : 'coordTrInt -> 'coordTrInt =
        (let finish : 'coordTrInt -> 'coordTrInt -> 'coordTrInt -> 
                      ('coordTrInt * 'bool) =
           (fun newroot  : 'coordTrInt. 
           (fun newleft  : 'coordTrInt.
           (fun newright : 'coordTrInt.
              (((setleftc ((setrightc newroot) newright)) newleft),false)))) in
	(let ruleLL : 'coordTrInt -> ('coordTrInt * 'bool) =
           (fun tree:'coordTrInt .
              (case (isblack tree)
                 x. (tree,true)
                 x. (case (isred (leftchild tree))
                 x. (tree,true)
                 x. (case (isred (leftchild (leftchild tree)))
                 x. (tree,true)
                 x. (let newright:'coordTrInt =
                      ((setleftc tree) 
                       (rightchild (leftchild tree))) in
                    (let newleft:'coordTrInt =
                       ((setcolor (leftchild (leftchild tree))) blackp) in
                    (((finish (leftchild tree)) newleft) newright))))))) in
	(let ruleRR : 'coordTrInt -> ('coordTrInt * 'bool) =
             (fun tree:'coordTrInt . 
                (case (isblack tree)
                 x. (tree,true)
                 x. (case (isred (rightchild tree))
                 x. (tree,true)
                 x. (case (isred (rightchild (rightchild tree)))
                 x. (tree,true)
                 x. (let newleft:'coordTrInt =
                      ((setrightc tree) 
                       (leftchild (rightchild tree))) in
                    (let newright:'coordTrInt =
                       ((setcolor (rightchild (rightchild tree))) blackp) in
	            (((finish (rightchild tree)) newleft) newright))))))) in
	(let ruleLR : 'coordTrInt -> ('coordTrInt * 'bool) =
           (fun tree:'coordTrInt .
              (case (isblack tree)
                 x. (tree,true)
                 x. (case (isred (leftchild tree))
                 x. (tree,true)
                 x. (case (isred (rightchild (leftchild tree)))
                 x. (tree,true)
                 x. (let newright:'coordTrInt =
                      ((setleftc tree) 
                       (rightchild (rightchild (leftchild tree)))) in
                    (let newleft:'coordTrInt =
                      ((setcolor 
                       ((setrightc (leftchild tree))
                        (leftchild (rightchild (leftchild tree))))) blackp) in
                    (((finish (rightchild (leftchild tree))) 
                              newleft) newright))))))) in
	(let ruleRL : 'coordTrInt -> ('coordTrInt * 'bool) =
           (fun tree:'coordTrInt .
              (case (isblack tree)
                 x. (tree,true)
                 x. (case (isred (rightchild tree))
                 x. (tree,true)
                 x. (case (isred (leftchild (rightchild tree)))
                 x. (tree,true)
                 x. (let newleft:'coordTrInt =
                      ((setrightc tree) 
                       (leftchild (leftchild (rightchild tree)))) in
                    (let newright:'coordTrInt =
                      ((setcolor
                       ((setleftc (rightchild tree))
                       (rightchild (leftchild (rightchild tree))))) blackp) in
                    (((finish (leftchild (rightchild tree))) 
                              newleft) newright))))))) in
     	(fun tree : 'coordTrInt. 
          (let pr:'coordTrInt *'bool = (ruleLL tree) in
          (case pr.2 x. pr.1 
           x. (let pr:'coordTrInt *'bool = (ruleLR tree) in
          (case pr.2 x. pr.1 
           x. (let pr:'coordTrInt *'bool = (ruleRL tree) in
          (case pr.2 x. pr.1 
           x. (let pr:'coordTrInt *'bool = (ruleRR tree) in
	   pr.1)))))))))))))
     in 

     (fun key : 'int.
     (fun tree: 'coordTrInt. 
       (let insertkey : 'coordTrInt -> 'coordTrInt =
           (fix (fun insertkey: 'coordTrInt -> 'coordTrInt .
                (fun tree : 'coordTrInt.
                  (unpack key as 'inktyp,ink in
                  (unpack tree as 'trlsttyp,tr in
                  (peel tr as {'ahd,'atla,'atlb},ptr in
                  (match (unroll (ptr.1))
                   uptr. ((((((((mkTree ['trlsttyp]) ['trlsttyp])
	                         key) redp) tr.1) tr.1) tr.2) tr.2)
                   uptr. 
                     (unpack (uptr.1) as 'trktyp,treek in
                     (ifG ink,treek
                      then (match ((unroll (ptr.1)).1,(unroll (ptr.2)))
                            uptrtwo. tree
                            uptrtwo. 
	 		      (balance ((setrightc tree)
                                        (insertkey (rightchild tree)))))
                      else (match ((unroll (ptr.1)).1,(unroll (ptr.2)))
                            uptrtwo. tree
                            uptrtwo. 
	 		      (balance ((setleftc tree)
                                        (insertkey (leftchild tree))))))))))))))
          in ((setcolor (insertkey tree)) blackp)))))))))))))))))))
in


(let six     : 'int = (pack 6,6     as 'int) in
(let eleven  : 'int = (pack 11,11   as 'int) in
(let two     : 'int = (pack 2,2     as 'int) in
(let hundred : 'int = (pack 100,100 as 'int) in
(let five    : 'int = (pack 5,5     as 'int) in
(let one     : 'int = (pack 1,1     as 'int) in


(type_abbrev 'coordTrAbs = 
  exists 'rblst:L(1,2)
    ((mu('rblst<-{'b}){'aone,'atwo} 
    	('b*(if 'b then unit else ('keytyp * ('aone * 'atwo)))))
     * (mu('rblst<-{'b}){'aone,'atwo} 
        (if 'b then S(0) else ('color * ('aone * 'atwo)))))
in
(let tester : all 'keytyp:T 
               ('keytyp -> 'keytyp -> 'keytyp -> 'keytyp -> 'keytyp -> 'keytyp 
	        -> 'coordTrAbs 
                -> ('keytyp -> 'coordTrAbs -> 'bool)
	        -> ('keytyp -> 'coordTrAbs -> 'coordTrAbs)
                -> ('bool*('bool*('bool*('bool*('bool*('bool*'coordTrAbs)))))))=
(fun 'keytyp:T . 
   (fun six:'keytyp . (fun eleven:'keytyp . (fun two:'keytyp .
   (fun hundred:'keytyp . (fun five:'keytyp . (fun one:'keytyp .
   (fun emptytree : 'coordTrAbs .
   (fun lookup : 'keytyp -> 'coordTrAbs -> 'bool .
   (fun insert : 'keytyp -> 'coordTrAbs -> 'coordTrAbs. 
      (let tree : 'coordTrAbs = 
       ((insert six) ((insert eleven) ((insert two) ((insert five) ((insert one)
         emptytree))))) in
         (((lookup hundred) tree), (((lookup eleven) tree), 
  	  (((lookup six)    tree), (((lookup two)    tree), 
          (((lookup five)   tree), (((lookup one)    tree),
	   tree)))))))))))))))))
in
((((((((((tester ['int]) six) eleven) two) hundred) five) one)
	emptytree) lookup) insert)
))))))))))))))))))))))