DEFINITION lift1_cons_tail()
TYPE =
       ∀t:T
         .∀h:nat
           .∀d:nat.∀hds:PList.(eq T (lift1 (PConsTail hds h d) t) (lift1 hds (lift h d t)))
BODY =
Show proof