DEFINITION nf2_lref_abst()
TYPE =
       ∀c:C
         .∀e:C
           .∀u:T.∀i:nat.(getl i c (CHead e (Bind Abst) u))→(nf2 c (TLRef i))
BODY =
        assume c: C
        assume e: C
        assume u: T
        assume i: nat
        suppose H: getl i c (CHead e (Bind Abst) u)
          we must prove nf2 c (TLRef i)
          or equivalently ∀t2:T.(pr2 c (TLRef i) t2)→(eq T (TLRef i) t2)
           assume t2: T
           suppose H0: pr2 c (TLRef i) t2
             (H1) 
                by (pr2_gen_lref . . . H0)

                   or
                     eq T t2 (TLRef i)
                     ex2_2
                       C
                       T
                       λd:C.λu:T.getl i c (CHead d (Bind Abbr) u)
                       λ:C.λu:T.eq T t2 (lift (S i) O u)
             end of H1
             we proceed by induction on H1 to prove eq T (TLRef i) t2
                case or_introl : H2:eq T t2 (TLRef i) ⇒
                   the thesis becomes eq T (TLRef i) t2
                      by (refl_equal . .)
                      we proved eq T (TLRef i) (TLRef i)
                      by (eq_ind_r . . . previous . H2)
eq T (TLRef i) t2
                case or_intror : H2:ex2_2 C T λd:C.λu0:T.getl i c (CHead d (Bind Abbr) u0) λ:C.λu0:T.eq T t2 (lift (S i) O u0) ⇒
                   the thesis becomes eq T (TLRef i) t2
                      we proceed by induction on H2 to prove eq T (TLRef i) t2
                         case ex2_2_intro : x0:C x1:T H3:getl i c (CHead x0 (Bind Abbr) x1) H4:eq T t2 (lift (S i) O x1) ⇒
                            the thesis becomes eq T (TLRef i) t2
                               (H6) 
                                  by (getl_mono . . . H . H3)
                                  we proved eq C (CHead e (Bind Abst) u) (CHead x0 (Bind Abbr) x1)
                                  we proceed by induction on the previous result to prove 
                                     <λ:C.Prop>
                                       CASE CHead x0 (Bind Abbr) x1 OF
                                         CSort ⇒False
                                       | CHead  k ⇒
                                             <λ:K.Prop>
                                               CASE k OF
                                                 Bind b⇒<λ:B.Prop> CASE b OF Abbr⇒False | Abst⇒True | Void⇒False
                                               | Flat ⇒False
                                     case refl_equal : ⇒
                                        the thesis becomes 
                                        <λ:C.Prop>
                                          CASE CHead e (Bind Abst) u OF
                                            CSort ⇒False
                                          | CHead  k ⇒
                                                <λ:K.Prop>
                                                  CASE k OF
                                                    Bind b⇒<λ:B.Prop> CASE b OF Abbr⇒False | Abst⇒True | Void⇒False
                                                  | Flat ⇒False
                                           consider I
                                           we proved True

                                              <λ:C.Prop>
                                                CASE CHead e (Bind Abst) u OF
                                                  CSort ⇒False
                                                | CHead  k ⇒
                                                      <λ:K.Prop>
                                                        CASE k OF
                                                          Bind b⇒<λ:B.Prop> CASE b OF Abbr⇒False | Abst⇒True | Void⇒False
                                                        | Flat ⇒False

                                     <λ:C.Prop>
                                       CASE CHead x0 (Bind Abbr) x1 OF
                                         CSort ⇒False
                                       | CHead  k ⇒
                                             <λ:K.Prop>
                                               CASE k OF
                                                 Bind b⇒<λ:B.Prop> CASE b OF Abbr⇒False | Abst⇒True | Void⇒False
                                               | Flat ⇒False
                               end of H6
                               consider H6
                               we proved 
                                  <λ:C.Prop>
                                    CASE CHead x0 (Bind Abbr) x1 OF
                                      CSort ⇒False
                                    | CHead  k ⇒
                                          <λ:K.Prop>
                                            CASE k OF
                                              Bind b⇒<λ:B.Prop> CASE b OF Abbr⇒False | Abst⇒True | Void⇒False
                                            | Flat ⇒False
                               that is equivalent to False
                               we proceed by induction on the previous result to prove eq T (TLRef i) (lift (S i) O x1)
                               we proved eq T (TLRef i) (lift (S i) O x1)
                               by (eq_ind_r . . . previous . H4)
eq T (TLRef i) t2
eq T (TLRef i) t2
             we proved eq T (TLRef i) t2
          we proved ∀t2:T.(pr2 c (TLRef i) t2)→(eq T (TLRef i) t2)
          that is equivalent to nf2 c (TLRef i)
       we proved 
          ∀c:C
            .∀e:C
              .∀u:T.∀i:nat.(getl i c (CHead e (Bind Abst) u))→(nf2 c (TLRef i))