DEFINITION nf2_csort_lref()
TYPE =
       ∀n:nat.∀i:nat.(nf2 (CSort n) (TLRef i))
BODY =
        assume n: nat
        assume i: nat
          we must prove nf2 (CSort n) (TLRef i)
          or equivalently ∀t2:T.(pr2 (CSort n) (TLRef i) t2)→(eq T (TLRef i) t2)
           assume t2: T
           suppose H: pr2 (CSort n) (TLRef i) t2
             (H0) 
                by (pr2_gen_lref . . . H)

                   or
                     eq T t2 (TLRef i)
                     ex2_2
                       C
                       T
                       λd:C.λu:T.getl i (CSort n) (CHead d (Bind Abbr) u)
                       λ:C.λu:T.eq T t2 (lift (S i) O u)
             end of H0
             we proceed by induction on H0 to prove eq T (TLRef i) t2
                case or_introl : H1: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 . H1)
eq T (TLRef i) t2
                case or_intror : H1:ex2_2 C T λd:C.λu:T.getl i (CSort n) (CHead d (Bind Abbr) u) λ:C.λu:T.eq T t2 (lift (S i) O u) ⇒
                   the thesis becomes eq T (TLRef i) t2
                      we proceed by induction on H1 to prove eq T (TLRef i) t2
                         case ex2_2_intro : x0:C x1:T H2:getl i (CSort n) (CHead x0 (Bind Abbr) x1) H3:eq T t2 (lift (S i) O x1) ⇒
                            the thesis becomes eq T (TLRef i) t2
                               by (getl_gen_sort . . . H2 .)
                               we proved eq T (TLRef i) (lift (S i) O x1)
                               by (eq_ind_r . . . previous . H3)
eq T (TLRef i) t2
eq T (TLRef i) t2
             we proved eq T (TLRef i) t2
          we proved ∀t2:T.(pr2 (CSort n) (TLRef i) t2)→(eq T (TLRef i) t2)
          that is equivalent to nf2 (CSort n) (TLRef i)
       we proved ∀n:nat.∀i:nat.(nf2 (CSort n) (TLRef i))