DEFINITION lifts1()
TYPE =
       PList→TList→TList
BODY =
FIXlifts1{
         lifts1:PList→TList→TList
         :=λhds:PList
           .λts:TList
             .<λt:TList.TList>
               CASE ts OF
                 TNil⇒TNil
               | TCons t ts0⇒TCons (lift1 hds t) (lifts1 hds ts0)
         }