DEFINITION lifts()
TYPE =
       nat→nat→TList→TList
BODY =
FIXlifts{
         lifts:nat→nat→TList→TList
         :=λh:nat
           .λd:nat
             .λts:TList
               .<λt:TList.TList>
                 CASE ts OF
                   TNil⇒TNil
                 | TCons t ts0⇒TCons (lift h d t) (lifts h d ts0)
         }