DEFINITION lift1_lref()
TYPE =
       ∀hds:PList.∀i:nat.(eq T (lift1 hds (TLRef i)) (TLRef (trans hds i)))
BODY =
Show proof