alloc : [x] . Unit -> rec t {l : <Cons {data : x,rest : rec t}#|Nil Unit> take};
map : [a, b]
      .
      {f : a -> b,list : rec t {l : <Cons {data : a,rest : rec t}#|Nil Unit>}!}#
      -> rec t {l : <Cons {data : b,rest : rec t}#|Nil Unit>};
map l = take l2 { list = node } = l : {f : a -> b
                                      ,list : rec t {l : <Cons {data : a
                                                               ,rest : rec t}#
                                                         |Nil Unit>}!}#
        in take l3 { f = fun } = l2 : {f : a -> b
                                      ,list : rec t {l : <Cons {data : a
                                                               ,rest : rec t}#
                                                         |Nil Unit>}! take}#
           in take node2 { l = head } = node : rec t {l : <Cons {data : a
                                                                ,rest : rec t}#
                                                          |Nil Unit>}!
              in case head : <Cons {data : a,rest : rec t}#|Nil Unit> of
                   Nil u -> let newNode = (alloc[b] : Unit
                                                      -> rec t {l : <Cons {data : b
                                                                          ,rest : rec t}#
                                                                    |Nil Unit> take}) (Unit : Unit) : rec t {l : <Cons {data : b
                                                                                                                       ,rest : rec t}#
                                                                                                                 |Nil Unit> take}
                            in put newNode : rec t {l : <Cons {data : b
                                                              ,rest : rec t}#
                                                        |Nil Unit> take}.l := Nil (Unit : Unit) : <Cons {data : b
                                                                                                        ,rest : rec t}#
                                                                                                  |Nil Unit>
                               end : rec t {l : <Cons {data : b,rest : rec t}#
                                                |Nil Unit>}
                            end : rec t {l : <Cons {data : b,rest : rec t}#
                                             |Nil Unit>}
                 | v2 -> case v2 : <Cons {data : a,rest : rec t}#
                                   |Nil Unit take> of
                           Cons remaining -> take remaining2 { data = x } = remaining : {data : a
                                                                                        ,rest : rec t}#
                                             in let newNode = (alloc[b] : Unit
                                                                          -> rec t {l : <Cons {data : b
                                                                                              ,rest : rec t}#
                                                                                        |Nil Unit> take}) (Unit : Unit) : rec t {l : <Cons {data : b
                                                                                                                                           ,rest : rec t}#
                                                                                                                                     |Nil Unit> take}
                                                in put newNode : rec t {l : <Cons {data : b
                                                                                  ,rest : rec t}#
                                                                            |Nil Unit> take}.l := Cons ({data = (fun : a
                                                                                                                       -> b) (x : a) : b
                                                                                                        ,rest = (map[ a
                                                                                                                    , b ] : {f : a
                                                                                                                                 -> b
                                                                                                                            ,list : rec t {l : <Cons {data : a
                                                                                                                                                     ,rest : rec t}#
                                                                                                                                               |Nil Unit>}!}#
                                                                                                                            -> rec t) ({list = (remaining2 : {data : a take
                                                                                                                                                             ,rest : rec t {l : <Cons {data : a
                                                                                                                                                                                      ,rest : rec t}#
                                                                                                                                                                                |Nil Unit>}!}#).rest : rec t {l : <Cons {data : a
                                                                                                                                                                                                                        ,rest : rec t}#
                                                                                                                                                                                                                  |Nil Unit>}!
                                                                                                                                       ,f = fun : a
                                                                                                                                                  -> b} : {f : a
                                                                                                                                                               -> b
                                                                                                                                                          ,list : rec t {l : <Cons {data : a
                                                                                                                                                                                   ,rest : rec t}#
                                                                                                                                                                             |Nil Unit>}!}#) : rec t} : {data : b
                                                                                                                                                                                                        ,rest : rec t}#) : <Cons {data : b
                                                                                                                                                                                                                                 ,rest : rec t}#
                                                                                                                                                                                                                           |Nil Unit>
                                                   end : rec t {l : <Cons {data : b
                                                                          ,rest : rec t}#
                                                                    |Nil Unit>}
                                                end : rec t {l : <Cons {data : b
                                                                       ,rest : rec t}#
                                                                 |Nil Unit>}
                                             end : rec t {l : <Cons {data : b
                                                                    ,rest : rec t}#
                                                              |Nil Unit>}
                         end : rec t {l : <Cons {data : b,rest : rec t}#
                                          |Nil Unit>}
                 end : rec t {l : <Cons {data : b,rest : rec t}#|Nil Unit>}
              end : rec t {l : <Cons {data : b,rest : rec t}#|Nil Unit>}
           end : rec t {l : <Cons {data : b,rest : rec t}#|Nil Unit>}
        end : rec t {l : <Cons {data : b,rest : rec t}#|Nil Unit>};