DEFINITION nf2_lift()
TYPE =
       ∀d:C.∀t:T.(nf2 d t)→∀c:C.∀h:nat.∀i:nat.(drop h i c d)→(nf2 c (lift h i t))
BODY =
Show proof