DEFINITION pr2_gen_csort()
TYPE =
       ∀t1:T.∀t2:T.∀n:nat.(pr2 (CSort n) t1 t2)→(pr0 t1 t2)
BODY =
        assume t1: T
        assume t2: T
        assume n: nat
        suppose H: pr2 (CSort n) t1 t2
           assume y: C
           suppose H0: pr2 y t1 t2
             we proceed by induction on H0 to prove (eq C y (CSort n))→(pr0 t1 t2)
                case pr2_free : c:C t3:T t4:T H1:pr0 t3 t4 ⇒
                      suppose : eq C c (CSort n)
                         consider H1
                case pr2_delta : c:C d:C u:T i:nat H1:getl i c (CHead d (Bind Abbr) u) t3:T t4:T :pr0 t3 t4 t:T :subst0 i u t4 t ⇒
                   the thesis becomes ∀H4:(eq C c (CSort n)).(pr0 t3 t)
                      suppose H4: eq C c (CSort n)
                         (H5) 
                            we proceed by induction on H4 to prove getl i (CSort n) (CHead d (Bind Abbr) u)
                               case refl_equal : ⇒
                                  the thesis becomes the hypothesis H1
getl i (CSort n) (CHead d (Bind Abbr) u)
                         end of H5
                         by (getl_gen_sort . . . H5 .)
                         we proved pr0 t3 t
∀H4:(eq C c (CSort n)).(pr0 t3 t)
             we proved (eq C y (CSort n))→(pr0 t1 t2)
          we proved ∀y:C.(pr2 y t1 t2)→(eq C y (CSort n))→(pr0 t1 t2)
          by (insert_eq . . . . previous H)
          we proved pr0 t1 t2
       we proved ∀t1:T.∀t2:T.∀n:nat.(pr2 (CSort n) t1 t2)→(pr0 t1 t2)