DEFINITION nf2_lift1()
TYPE =
       ∀e:C.∀hds:PList.∀c:C.∀t:T.(drop1 hds c e)→(nf2 e t)→(nf2 c (lift1 hds t))
BODY =
Show proof