delete : EmptyBox -> Unit;
insert : [a] . {box : EmptyBox,item : a}# -> Box a;
new : Unit -> EmptyBox;
remove : [a] . Box a -> {box : EmptyBox,item : a}#;
test : [x] . x -> x;
test x = let boxbox = (new[] : Unit -> EmptyBox) (Unit : Unit) : EmptyBox
         in let box = (new[] : Unit -> EmptyBox) (Unit : Unit) : EmptyBox
            in let full = (insert[x] : {box : EmptyBox,item : x}#
                                       -> Box x) ({box = box : EmptyBox
                                                  ,item = x : x} : {box : EmptyBox
                                                                   ,item : x}#) : Box x
               in let fullbox = (insert[Box x] : {box : EmptyBox,item : Box x}#
                                                 -> Box (Box x)) ({box = boxbox : EmptyBox
                                                                  ,item = full : Box x} : {box : EmptyBox
                                                                                          ,item : Box x}#) : Box (Box x)
                  in take r { box = b } = (remove[Box x] : Box (Box x)
                                                           -> {box : EmptyBox
                                                              ,item : Box x}#) (fullbox : Box (Box x)) : {box : EmptyBox
                                                                                                         ,item : Box x}#
                     in take r { item = i } = r : {box : EmptyBox take
                                                  ,item : Box x}#
                        in let u = (delete[] : EmptyBox
                                               -> Unit) (b : EmptyBox) : Unit
                           in take r { box = b } = (remove[x] : Box x
                                                                -> {box : EmptyBox
                                                                   ,item : x}#) (i : Box x) : {box : EmptyBox
                                                                                              ,item : x}#
                              in let u = (delete[] : EmptyBox
                                                     -> Unit) (b : EmptyBox) : Unit
                                 in take r { item = ret } = r : {box : EmptyBox take
                                                                ,item : x}#
                                    in ret : x
                                    end : x
                                 end : x
                              end : x
                           end : x
                        end : x
                     end : x
                  end : x
               end : x
            end : x
         end : x;