DEFINITION nf2_gen_lref()
TYPE =
       ∀c:C
         .∀d:C
           .∀u:T
             .∀i:nat
               .getl i c (CHead d (Bind Abbr) u)
                 →(nf2 c (TLRef i))→∀P:Prop.P
BODY =
        assume c: C
        assume d: C
        assume u: T
        assume i: nat
        suppose H: getl i c (CHead d (Bind Abbr) u)
          we must prove (nf2 c (TLRef i))→∀P:Prop.P
          or equivalently (∀t2:T.(pr2 c (TLRef i) t2)→(eq T (TLRef i) t2))→∀P:Prop.P
           suppose H0: ∀t2:T.(pr2 c (TLRef i) t2)→(eq T (TLRef i) t2)
           assume P: Prop
             (h1) by (le_O_n .) we proved le O i
             (h2) 
                by (le_n .)
                we proved le (plus O (S i)) (plus O (S i))
lt i (plus O (S i))
             end of h2
             (h3) 
                (h1) 
                   by (pr0_refl .)
pr0 (TLRef i) (TLRef i)
                end of h1
                (h2) 
                   by (subst0_lref . .)
subst0 i u (TLRef i) (lift (S i) O u)
                end of h2
                by (pr2_delta . . . . H . . h1 . h2)
                we proved pr2 c (TLRef i) (lift (S i) O u)
                by (H0 . previous)
eq T (TLRef i) (lift (S i) O u)
             end of h3
             by (lift_gen_lref_false . . . h1 h2 . h3 .)
             we proved P
          we proved (∀t2:T.(pr2 c (TLRef i) t2)→(eq T (TLRef i) t2))→∀P:Prop.P
          that is equivalent to (nf2 c (TLRef i))→∀P:Prop.P
       we proved 
          ∀c:C
            .∀d:C
              .∀u:T
                .∀i:nat
                  .getl i c (CHead d (Bind Abbr) u)
                    →(nf2 c (TLRef i))→∀P:Prop.P