DEFINITION pc3_gen_sort()
TYPE =
       ∀c:C.∀m:nat.∀n:nat.(pc3 c (TSort m) (TSort n))→(eq nat m n)
BODY =
        assume c: C
        assume m: nat
        assume n: nat
        suppose H: pc3 c (TSort m) (TSort n)
          (H0) consider H
          consider H0
          we proved pc3 c (TSort m) (TSort n)
          that is equivalent to ex2 T λt:T.pr3 c (TSort m) t λt:T.pr3 c (TSort n) t
          we proceed by induction on the previous result to prove eq nat m n
             case ex_intro2 : x:T H1:pr3 c (TSort m) x H2:pr3 c (TSort n) x ⇒
                the thesis becomes eq nat m n
                   (H3) 
                      by (pr3_gen_sort . . . H1)
                      we proved eq T x (TSort m)
                      we proceed by induction on the previous result to prove eq T (TSort m) (TSort n)
                         case refl_equal : ⇒
                            the thesis becomes eq T x (TSort n)
                               by (pr3_gen_sort . . . H2)
eq T x (TSort n)
eq T (TSort m) (TSort n)
                   end of H3
                   (H4) 
                      by (f_equal . . . . . H3)
                      we proved 
                         eq
                           nat
                           <λ:T.nat> CASE TSort m OF TSort n0⇒n0 | TLRef ⇒m | THead   ⇒m
                           <λ:T.nat> CASE TSort n OF TSort n0⇒n0 | TLRef ⇒m | THead   ⇒m

                         eq
                           nat
                           λe:T.<λ:T.nat> CASE e OF TSort n0⇒n0 | TLRef ⇒m | THead   ⇒m (TSort m)
                           λe:T.<λ:T.nat> CASE e OF TSort n0⇒n0 | TLRef ⇒m | THead   ⇒m (TSort n)
                   end of H4
                   consider H4
                   we proved 
                      eq
                        nat
                        <λ:T.nat> CASE TSort m OF TSort n0⇒n0 | TLRef ⇒m | THead   ⇒m
                        <λ:T.nat> CASE TSort n OF TSort n0⇒n0 | TLRef ⇒m | THead   ⇒m
eq nat m n
          we proved eq nat m n
       we proved ∀c:C.∀m:nat.∀n:nat.(pc3 c (TSort m) (TSort n))→(eq nat m n)