DEFINITION lift1_lift1()
TYPE =
       ∀is1:PList.∀is2:PList.∀t:T.(eq T (lift1 is1 (lift1 is2 t)) (lift1 (papp is1 is2) t))
BODY =
Show proof