DEFINITION pr3_gen_sort()
TYPE =
       ∀c:C.∀x:T.∀n:nat.(pr3 c (TSort n) x)→(eq T x (TSort n))
BODY =
        assume c: C
        assume x: T
        assume n: nat
        suppose H: pr3 c (TSort n) x
           assume y: T
           suppose H0: pr3 c y x
             we proceed by induction on H0 to prove (eq T y (TSort n))→(eq T x y)
                case pr3_refl : t:T ⇒
                   the thesis becomes (eq T t (TSort n))→(eq T t t)
                      suppose : eq T t (TSort n)
                         by (refl_equal . .)
                         we proved eq T t t
(eq T t (TSort n))→(eq T t t)
                case pr3_sing : t2:T t1:T H1:pr2 c t1 t2 t3:T :pr3 c t2 t3 ⇒
                   the thesis becomes ∀H4:(eq T t1 (TSort n)).(eq T t3 t1)
                   (H3) by induction hypothesis we know (eq T t2 (TSort n))→(eq T t3 t2)
                      suppose H4: eq T t1 (TSort n)
                         (H5) 
                            we proceed by induction on H4 to prove pr2 c (TSort n) t2
                               case refl_equal : ⇒
                                  the thesis becomes the hypothesis H1
pr2 c (TSort n) t2
                         end of H5
                         (H6) 
                            by (pr2_gen_sort . . . H5)
                            we proved eq T t2 (TSort n)
                            we proceed by induction on the previous result to prove (eq T (TSort n) (TSort n))→(eq T t3 (TSort n))
                               case refl_equal : ⇒
                                  the thesis becomes the hypothesis H3
(eq T (TSort n) (TSort n))→(eq T t3 (TSort n))
                         end of H6
                         by (refl_equal . .)
                         we proved eq T (TSort n) (TSort n)
                         by (H6 previous)
                         we proved eq T t3 (TSort n)
                         by (eq_ind_r . . . previous . H4)
                         we proved eq T t3 t1
∀H4:(eq T t1 (TSort n)).(eq T t3 t1)
             we proved (eq T y (TSort n))→(eq T x y)
          we proved ∀y:T.(pr3 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.(pr3 c (TSort n) x)→(eq T x (TSort n))