(type_abbrev 'oneStar =        ({S(1)}!(1)) in
(type_abbrev 'oneOneStar =     ({S(1)}::(1,1){'oneStar}) in
(type_abbrev 'zeroOneOneStar = ({S(0)}::(1,1){'oneOneStar}) in
(type_abbrev 'zZOOStar =       ({S(0)}::(1,1){'zeroOneOneStar}) in

(type_abbrev 'tagNode = ('b*(if 'b then unit else (unit*'a))) in
(type_abbrev 'noTagNode = (if 'b then unit else (unit*'a)) in
(type_abbrev 'pairNode = ('b*(if 'b then (unit*unit) else ((unit*unit)*'a))) in

(type_abbrev 'list_of_pairs = 
  (exists 'l:L(1,1) (mu('l<-{'b}){'a} 'pairNode)) in
(type_abbrev 'pair_of_lists =
  (exists 'l:L(1,1)((mu('l<-{'b}){'a} 'tagNode) * 
                    (mu('l<-{'b}){'a} 'noTagNode))) in

(type_abbrev 'empty_tagged =   (mu('oneOneStar<-{'b}){'a} 'tagNode) in
(type_abbrev 'empty_untagged = (mu('oneOneStar<-{'b}){'a} 'noTagNode) in
(type_abbrev 'empty_pair = (mu(({S(1)}::(1,1){'tllst})<-{'b}){'a} 'pairNode) in
(type_abbrev 'empty_unrolled_tagged =
  (if S(1) then unit else (unit*(mu('oneStar<-{'b}){'a} 'tagNode))) in
(type_abbrev 'empty_unrolled_untagged =
  (if S(1) then unit else (unit*(mu('oneStar<-{'b}){'a} 'noTagNode))) in

(let unzip_list : 'list_of_pairs -> 'pair_of_lists =
 (fix (fun unzip: 'list_of_pairs -> 'pair_of_lists .
  (fun zippedlist: 'list_of_pairs .
   (unpack zippedlist as 'l,zippedlist in
    (peel (zippedlist,zippedlist) as {'hd,'tl},zippedlist in
     (match (unroll (zippedlist.1))
       list.
        (pack 'oneOneStar,
         (roll (1,(tosum list.1,'empty_unrolled_tagged)) as 'empty_tagged,
          roll (tosum list.2,'empty_unrolled_untagged) as 'empty_untagged)
         as 'pair_of_lists)
       list.
        (unpack (unzip pack 'tl,list.2 as 'list_of_pairs) as 'tltyp,tllists in
         (type_abbrev 'newLstT = ({S(0)}::(1,1){'tltyp}) in
          (pack 'newLstT,
           (roll (0,(tosum (list.1.1,tllists.1),
              if S(0) then unit else (unit*(mu('tltyp<-{'b}){'a} 'tagNode))))
            as (mu('newLstT<-{'b}){'a} 'tagNode),
            roll (tosum (list.1.2,tllists.2),
              if S(0) then unit else (unit*(mu('tltyp<-{'b}){'a} 'noTagNode)))
            as (mu('newLstT<-{'b}){'a} 'noTagNode))
           as 'pair_of_lists))))))))) in

(let zip_lists : 'pair_of_lists -> 'list_of_pairs =
 (fix (fun zip : 'pair_of_lists -> 'list_of_pairs .  
  (fun clist: 'pair_of_lists .
   (unpack clist as 'l,dlist in
    (peel dlist as {'hd,'tllst},elist in
     (match (unroll (elist.1))
       listone.
        (pack ({S(1)}::(1,1){'tllst}), 
         (roll (1,(tosum (listone, (match ((unroll elist.1).1,(unroll elist.2))
                                     listtwo. listtwo
                                     listtwo. (listtwo.1))),
                         if S(1) then (unit*unit) 
                         else ((unit*unit)*(mu('tllst<-{'b}){'a} 'pairNode))))
          as 'empty_pair)
         as 'list_of_pairs) 
       listone. 
        (unpack (zip (match ((unroll elist.1).1, (unroll elist.2))
                       listtwo. clist
                       listtwo. 
                         pack 'tllst,(listone.2,listtwo.2) as 'pair_of_lists)) 
         as 'tltyp,zippedtail in  
          (pack ({S(0)}::(1,1){'tltyp}),
            (roll (0,(tosum ((listone.1,
                             (match ((unroll elist.1).1,(unroll elist.2))
                               listtwo. listtwo
                               listtwo. listtwo.1)), zippedtail),
                          if S(0) then (unit*unit) 
                          else ((unit*unit)*(mu('tltyp<-{'b}){'a} 'pairNode))))
             as (mu(({S(0)}::(1,1){'tltyp})<-{'b}){'a} 'pairNode))
           as 'list_of_pairs)))))))) in

(let empty : 'empty_tagged*'empty_untagged =
  (roll (1,(tosum (),'empty_unrolled_tagged)) as 'empty_tagged,
   roll (tosum (),'empty_unrolled_untagged) as 'empty_untagged) in

(let oneEl : 
 (mu('zeroOneOneStar<-{'b}){'a} 'tagNode) * 
 (mu('zeroOneOneStar<-{'b}){'a} 'noTagNode) =
  (roll (0,(tosum ((),empty.1), 
     if S(0) then unit else (unit*(mu('oneOneStar<-{'b}){'a} 'tagNode))))
   as (mu('zeroOneOneStar<-{'b}){'a} 'tagNode),
   roll (tosum ((),empty.2), 
     if S(0) then unit else (unit*(mu('oneOneStar<-{'b}){'a} 'noTagNode))) 
   as (mu('zeroOneOneStar<-{'b}){'a} 'noTagNode)) in

(let twoElListPair : 'pair_of_lists =
 (pack 'zZOOStar,
  (roll (0,(tosum ((),oneEl.1),
     if S(0) then unit else (unit*(mu('zeroOneOneStar<-{'b}){'a} 'tagNode))))
   as (mu('zZOOStar<-{'b}){'a} 'tagNode),
   roll (tosum ((),oneEl.2),
     if S(0) then unit else (unit*(mu('zeroOneOneStar<-{'b}){'a} 'noTagNode)))
   as (mu('zZOOStar<-{'b}){'a} 'noTagNode))
  as 'pair_of_lists) in

(unzip_list (zip_lists twoElListPair)))))))))))))))))))))