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 =
        assume d: C
        assume t: T
          we must prove (nf2 d t)→∀c:C.∀h:nat.∀i:nat.(drop h i c d)→(nf2 c (lift h i t))
          or equivalently 
                ∀t2:T.(pr2 d t t2)→(eq T t t2)
                  →∀c:C.∀h:nat.∀i:nat.(drop h i c d)→(nf2 c (lift h i t))
           suppose H: ∀t2:T.(pr2 d t t2)→(eq T t t2)
           assume c: C
           assume h: nat
           assume i: nat
           suppose H0: drop h i c d
             we must prove nf2 c (lift h i t)
             or equivalently ∀t2:T.(pr2 c (lift h i t) t2)→(eq T (lift h i t) t2)
              assume t2: T
              suppose H1: pr2 c (lift h i t) t2
                (H2) 
                   by (pr2_gen_lift . . . . . H1 . H0)
ex2 T λt2:T.eq T t2 (lift h i t2) λt2:T.pr2 d t t2
                end of H2
                we proceed by induction on H2 to prove eq T (lift h i t) t2
                   case ex_intro2 : x:T H3:eq T t2 (lift h i x) H4:pr2 d t x ⇒
                      the thesis becomes eq T (lift h i t) t2
                         (H_y) by (H . H4) we proved eq T t x
                         we proceed by induction on H_y to prove eq T (lift h i t) (lift h i x)
                            case refl_equal : ⇒
                               the thesis becomes eq T (lift h i t) (lift h i t)
                                  by (refl_equal . .)
eq T (lift h i t) (lift h i t)
                         we proved eq T (lift h i t) (lift h i x)
                         by (eq_ind_r . . . previous . H3)
eq T (lift h i t) t2
                we proved eq T (lift h i t) t2
             we proved ∀t2:T.(pr2 c (lift h i t) t2)→(eq T (lift h i t) t2)
             that is equivalent to nf2 c (lift h i t)
          we proved 
             ∀t2:T.(pr2 d t t2)→(eq T t t2)
               →∀c:C.∀h:nat.∀i:nat.(drop h i c d)→(nf2 c (lift h i t))
          that is equivalent to (nf2 d t)→∀c:C.∀h:nat.∀i:nat.(drop h i c d)→(nf2 c (lift h i t))
       we proved ∀d:C.∀t:T.(nf2 d t)→∀c:C.∀h:nat.∀i:nat.(drop h i c d)→(nf2 c (lift h i t))