DEFINITION pr2_gen_sort()
TYPE =
       ∀c:C.∀x:T.∀n:nat.(pr2 c (TSort n) x)→(eq T x (TSort n))
BODY =
        assume c: C
        assume x: T
        assume n: nat
        suppose H: pr2 c (TSort n) x
           assume y: T
           suppose H0: pr2 c y x
             we proceed by induction on H0 to prove (eq T y (TSort n))→(eq T x y)
                case pr2_free : :C t1:T t2:T H1:pr0 t1 t2 ⇒
                   the thesis becomes ∀H2:(eq T t1 (TSort n)).(eq T t2 t1)
                      suppose H2: eq T t1 (TSort n)
                         (H3) 
                            we proceed by induction on H2 to prove pr0 (TSort n) t2
                               case refl_equal : ⇒
                                  the thesis becomes the hypothesis H1
pr0 (TSort n) t2
                         end of H3
                         (h1) 
                            by (refl_equal . .)
eq T (TSort n) (TSort n)
                         end of h1
                         (h2) 
                            by (pr0_gen_sort . . H3)
eq T t2 (TSort n)
                         end of h2
                         by (eq_ind_r . . . h1 . h2)
                         we proved eq T t2 (TSort n)
                         by (eq_ind_r . . . previous . H2)
                         we proved eq T t2 t1
∀H2:(eq T t1 (TSort n)).(eq T t2 t1)
                case pr2_delta : c0:C d:C u:T i:nat :getl i c0 (CHead d (Bind Abbr) u) t1:T t2:T H2:pr0 t1 t2 t:T H3:subst0 i u t2 t ⇒
                   the thesis becomes ∀H4:(eq T t1 (TSort n)).(eq T t t1)
                      suppose H4: eq T t1 (TSort n)
                         (H5) 
                            we proceed by induction on H4 to prove pr0 (TSort n) t2
                               case refl_equal : ⇒
                                  the thesis becomes the hypothesis H2
pr0 (TSort n) t2
                         end of H5
                         (H6) 
                            by (pr0_gen_sort . . H5)
                            we proved eq T t2 (TSort n)
                            we proceed by induction on the previous result to prove subst0 i u (TSort n) t
                               case refl_equal : ⇒
                                  the thesis becomes the hypothesis H3
subst0 i u (TSort n) t
                         end of H6
                         by (subst0_gen_sort . . . . H6 .)
                         we proved eq T t (TSort n)
                         by (eq_ind_r . . . previous . H4)
                         we proved eq T t t1
∀H4:(eq T t1 (TSort n)).(eq T t t1)
             we proved (eq T y (TSort n))→(eq T x y)
          we proved ∀y:T.(pr2 c y x)→(eq T y (TSort n))→(eq T x y)
          by (insert_eq . . . . previous H)
          we proved eq T x (TSort n)
       we proved ∀c:C.∀x:T.∀n:nat.(pr2 c (TSort n) x)→(eq T x (TSort n))