DEFINITION nf2_sort()
TYPE =
       ∀c:C.∀n:nat.(nf2 c (TSort n))
BODY =
        assume c: C
        assume n: nat
          we must prove nf2 c (TSort n)
          or equivalently ∀t2:T.(pr2 c (TSort n) t2)→(eq T (TSort n) t2)
           assume t2: T
           suppose H: pr2 c (TSort n) t2
             (h1) 
                by (refl_equal . .)
eq T (TSort n) (TSort n)
             end of h1
             (h2) 
                by (pr2_gen_sort . . . H)
eq T t2 (TSort n)
             end of h2
             by (eq_ind_r . . . h1 . h2)
             we proved eq T (TSort n) t2
          we proved ∀t2:T.(pr2 c (TSort n) t2)→(eq T (TSort n) t2)
          that is equivalent to nf2 c (TSort n)
       we proved ∀c:C.∀n:nat.(nf2 c (TSort n))