DEFINITION lift1_free()
TYPE =
       ∀hds:PList
         .∀i:nat
           .∀t:T
             .eq
               T
               lift1 hds (lift (S i) O t)
               lift (S (trans hds i)) O (lift1 (ptrans hds i) t)
BODY =
Show proof