DEFINITION wcpr0_gen_sort()
TYPE =
       ∀x:C.∀n:nat.(wcpr0 (CSort n) x)→(eq C x (CSort n))
BODY =
        assume x: C
        assume n: nat
        suppose H: wcpr0 (CSort n) x
           assume y: C
           suppose H0: wcpr0 y x
             we proceed by induction on H0 to prove (eq C y (CSort n))→(eq C x y)
                case wcpr0_refl : c:C ⇒
                   the thesis becomes ∀H1:(eq C c (CSort n)).(eq C c c)
                      suppose H1: eq C c (CSort n)
                         (H2) 
                            by (f_equal . . . . . H1)
                            we proved eq C c (CSort n)
eq C (λe:C.e c) (λe:C.e (CSort n))
                         end of H2
                         by (refl_equal . .)
                         we proved eq C (CSort n) (CSort n)
                         by (eq_ind_r . . . previous . H2)
                         we proved eq C c c
∀H1:(eq C c (CSort n)).(eq C c c)
                case wcpr0_comp : c1:C c2:C :wcpr0 c1 c2 u1:T u2:T :pr0 u1 u2 k:K ⇒
                   the thesis becomes ∀H4:(eq C (CHead c1 k u1) (CSort n)).(eq C (CHead c2 k u2) (CHead c1 k u1))
                   () by induction hypothesis we know (eq C c1 (CSort n))→(eq C c2 c1)
                      suppose H4: eq C (CHead c1 k u1) (CSort n)
                         (H5) 
                            we proceed by induction on H4 to prove <λ:C.Prop> CASE CSort n OF CSort ⇒False | CHead   ⇒True
                               case refl_equal : ⇒
                                  the thesis becomes <λ:C.Prop> CASE CHead c1 k u1 OF CSort ⇒False | CHead   ⇒True
                                     consider I
                                     we proved True
<λ:C.Prop> CASE CHead c1 k u1 OF CSort ⇒False | CHead   ⇒True
<λ:C.Prop> CASE CSort n OF CSort ⇒False | CHead   ⇒True
                         end of H5
                         consider H5
                         we proved <λ:C.Prop> CASE CSort n OF CSort ⇒False | CHead   ⇒True
                         that is equivalent to False
                         we proceed by induction on the previous result to prove eq C (CHead c2 k u2) (CHead c1 k u1)
                         we proved eq C (CHead c2 k u2) (CHead c1 k u1)
∀H4:(eq C (CHead c1 k u1) (CSort n)).(eq C (CHead c2 k u2) (CHead c1 k u1))
             we proved (eq C y (CSort n))→(eq C x y)
          we proved ∀y:C.(wcpr0 y x)→(eq C y (CSort n))→(eq C x y)
          by (insert_eq . . . . previous H)
          we proved eq C x (CSort n)
       we proved ∀x:C.∀n:nat.(wcpr0 (CSort n) x)→(eq C x (CSort n))