DEFINITION lift1()
TYPE =
       PList→T→T
BODY =
FIXlift1{
         lift1:PList→T→T
         :=λhds:PList.λt:T.<λp:PList.T> CASE hds OF PNil⇒t | PCons h d hds0⇒lift h d (lift1 hds0 t)
         }