DEFINITION pc3_gen_sort_abst()
TYPE =
       ∀c:C.∀u:T.∀t:T.∀n:nat.(pc3 c (TSort n) (THead (Bind Abst) u t))→∀P:Prop.P
BODY =
        assume c: C
        assume u: T
        assume t: T
        assume n: nat
        suppose H: pc3 c (TSort n) (THead (Bind Abst) u t)
        assume P: Prop
          (H0) consider H
          consider H0
          we proved pc3 c (TSort n) (THead (Bind Abst) u t)
          that is equivalent to ex2 T λt0:T.pr3 c (TSort n) t0 λt0:T.pr3 c (THead (Bind Abst) u t) t0
          we proceed by induction on the previous result to prove P
             case ex_intro2 : x:T H1:pr3 c (TSort n) x H2:pr3 c (THead (Bind Abst) u t) x ⇒
                the thesis becomes P
                   (H3) 
                      by (pr3_gen_abst . . . . H2)

                         ex3_2
                           T
                           T
                           λu2:T.λt2:T.eq T x (THead (Bind Abst) u2 t2)
                           λu2:T.λ:T.pr3 c u u2
                           λ:T.λt2:T.∀b:B.∀u:T.(pr3 (CHead c (Bind b) u) t t2)
                   end of H3
                   we proceed by induction on H3 to prove P
                      case ex3_2_intro : x0:T x1:T H4:eq T x (THead (Bind Abst) x0 x1) :pr3 c u x0 :∀b:B.∀u0:T.(pr3 (CHead c (Bind b) u0) t x1) ⇒
                         the thesis becomes P
                            (H7) 
                               we proceed by induction on H4 to prove eq T (THead (Bind Abst) x0 x1) (TSort n)
                                  case refl_equal : ⇒
                                     the thesis becomes eq T x (TSort n)
                                        by (pr3_gen_sort . . . H1)
eq T x (TSort n)
eq T (THead (Bind Abst) x0 x1) (TSort n)
                            end of H7
                            (H8) 
                               we proceed by induction on H7 to prove 
                                  <λ:T.Prop>
                                    CASE TSort n OF
                                      TSort ⇒False
                                    | TLRef ⇒False
                                    | THead   ⇒True
                                  case refl_equal : ⇒
                                     the thesis becomes 
                                     <λ:T.Prop>
                                       CASE THead (Bind Abst) x0 x1 OF
                                         TSort ⇒False
                                       | TLRef ⇒False
                                       | THead   ⇒True
                                        consider I
                                        we proved True

                                           <λ:T.Prop>
                                             CASE THead (Bind Abst) x0 x1 OF
                                               TSort ⇒False
                                             | TLRef ⇒False
                                             | THead   ⇒True

                                  <λ:T.Prop>
                                    CASE TSort n OF
                                      TSort ⇒False
                                    | TLRef ⇒False
                                    | THead   ⇒True
                            end of H8
                            consider H8
                            we proved 
                               <λ:T.Prop>
                                 CASE TSort n OF
                                   TSort ⇒False
                                 | TLRef ⇒False
                                 | THead   ⇒True
                            that is equivalent to False
                            we proceed by induction on the previous result to prove P
P
P
          we proved P
       we proved 
          ∀c:C.∀u:T.∀t:T.∀n:nat.(pc3 c (TSort n) (THead (Bind Abst) u t))→∀P:Prop.P