allocNode : [a]
            .
            Unit -> rec t {l : <Cons {data : a,rest : rec t}#|Nil Unit> take};
createEmptyList : [a]
                  .
                  U8 -> rec t {l : <Cons {data : a,rest : rec t}#|Nil Unit>};
createEmptyList a = let node = (allocNode[a] : Unit
                                               -> rec t {l : <Cons {data : a
                                                                   ,rest : rec t}#
                                                             |Nil Unit> take}) (Unit : Unit) : rec t {l : <Cons {data : a
                                                                                                                ,rest : rec t}#
                                                                                                          |Nil Unit> take}
                    in put node : rec t {l : <Cons {data : a,rest : rec t}#
                                             |Nil Unit> take}.l := Nil (Unit : Unit) : <Cons {data : a
                                                                                             ,rest : rec t}#
                                                                                       |Nil Unit>
                       end : rec t {l : <Cons {data : a,rest : rec t}#
                                        |Nil Unit>}
                    end : rec t {l : <Cons {data : a,rest : rec t}#|Nil Unit>};