alloc : Unit -> rec t {l : <Cons {d : U8,r : rec t}#|End Unit> take};
makeEmptyList : Unit -> rec t {l : <Cons {d : U8,r : rec t}#|End Unit>};
makeEmptyList a = let r = (alloc[] : Unit
                                     -> rec t {l : <Cons {d : U8,r : rec t}#
                                                   |End Unit> take}) (Unit : Unit) : rec t {l : <Cons {d : U8
                                                                                                      ,r : rec t}#
                                                                                                |End Unit> take}
                  in put r : rec t {l : <Cons {d : U8,r : rec t}#
                                        |End Unit> take}.l := End (Unit : Unit) : <Cons {d : U8
                                                                                        ,r : rec t}#
                                                                                  |End Unit>
                     end : rec t {l : <Cons {d : U8,r : rec t}#|End Unit>}
                  end : rec t {l : <Cons {d : U8,r : rec t}#|End Unit>};