DEFINITION ty3_predicative()
TYPE =
       ∀g:G
         .∀c:C
           .∀v:T.∀t:T.∀u:T.(ty3 g c (THead (Bind Abst) v t) u)→(pc3 c u v)→∀P:Prop.P
BODY =
        assume g: G
        assume c: C
        assume v: T
        assume t: T
        assume u: T
        suppose H: ty3 g c (THead (Bind Abst) v t) u
        suppose H0: pc3 c u v
        assume P: Prop
          (H1) consider H
          by (ty3_gen_bind . . . . . . H1)
          we proved 
             ex3_2
               T
               T
               λt2:T.λ:T.pc3 c (THead (Bind Abst) v t2) u
               λ:T.λt:T.ty3 g c v t
               λt2:T.λ:T.ty3 g (CHead c (Bind Abst) v) t t2
          we proceed by induction on the previous result to prove P
             case ex3_2_intro : x0:T x1:T :pc3 c (THead (Bind Abst) v x0) u H3:ty3 g c v x1 :ty3 g (CHead c (Bind Abst) v) t x0 ⇒
                the thesis becomes P
                   (H_y) 
                      by (ty3_conv . . . . H3 . . H H0)
ty3 g c (THead (Bind Abst) v t) v
                   end of H_y
                   (H_x) 
                      by (ty3_arity . . . . H_y)

                         ex2
                           A
                           λa1:A.arity g c (THead (Bind Abst) v t) a1
                           λa1:A.arity g c v (asucc g a1)
                   end of H_x
                   (H5) consider H_x
                   we proceed by induction on H5 to prove P
                      case ex_intro2 : x:A H6:arity g c (THead (Bind Abst) v t) x H7:arity g c v (asucc g x) ⇒
                         the thesis becomes P
                            (H8) 
                               by (arity_gen_abst . . . . . H6)

                                  ex3_2
                                    A
                                    A
                                    λa1:A.λa2:A.eq A x (AHead a1 a2)
                                    λa1:A.λ:A.arity g c v (asucc g a1)
                                    λ:A.λa2:A.arity g (CHead c (Bind Abst) v) t a2
                            end of H8
                            we proceed by induction on H8 to prove P
                               case ex3_2_intro : x2:A x3:A H9:eq A x (AHead x2 x3) H10:arity g c v (asucc g x2) :arity g (CHead c (Bind Abst) v) t x3 ⇒
                                  the thesis becomes P
                                     (H12) 
                                        we proceed by induction on H9 to prove arity g c v (asucc g (AHead x2 x3))
                                           case refl_equal : ⇒
                                              the thesis becomes the hypothesis H7
arity g c v (asucc g (AHead x2 x3))
                                     end of H12
                                     by (arity_mono . . . . H12 . H10)
                                     we proved leq g (asucc g (AHead x2 x3)) (asucc g x2)
                                     that is equivalent to leq g (AHead x2 (asucc g x3)) (asucc g x2)
                                     by (leq_ahead_asucc_false . . . previous .)
P
P
P
          we proved P
       we proved 
          ∀g:G
            .∀c:C
              .∀v:T.∀t:T.∀u:T.(ty3 g c (THead (Bind Abst) v t) u)→(pc3 c u v)→∀P:Prop.P