DEFINITION ty3_repellent()
TYPE =
       ∀g:G
         .∀c:C
           .∀w:T
             .∀t:T
               .∀u1:T
                 .ty3 g c (THead (Bind Abst) w t) u1
                   →∀u2:T
                        .ty3 g (CHead c (Bind Abst) w) t (lift (S O) O u2)
                          →(pc3 c u1 u2)→∀P:Prop.P
BODY =
        assume g: G
        assume c: C
        assume w: T
        assume t: T
        assume u1: T
        suppose H: ty3 g c (THead (Bind Abst) w t) u1
        assume u2: T
        suppose H0: ty3 g (CHead c (Bind Abst) w) t (lift (S O) O u2)
        suppose H1: pc3 c u1 u2
        assume P: Prop
          by (ty3_correct . . . . H0)
          we proved ex T λt:T.ty3 g (CHead c (Bind Abst) w) (lift (S O) O u2) t
          we proceed by induction on the previous result to prove P
             case ex_intro : x:T H2:ty3 g (CHead c (Bind Abst) w) (lift (S O) O u2) x ⇒
                the thesis becomes P
                   (H3) 
                      by (drop_refl .)
                      we proved drop O O c c
                      that is equivalent to drop (r (Bind Abst) O) O c c
                      by (drop_drop . . . . previous .)
                      we proved drop (S O) O (CHead c (Bind Abst) w) c
                      by (ty3_gen_lift . . . . . . H2 . previous)
ex2 T λt2:T.pc3 (CHead c (Bind Abst) w) (lift (S O) O t2) x λt2:T.ty3 g c u2 t2
                   end of H3
                   we proceed by induction on H3 to prove P
                      case ex_intro2 : x0:T :pc3 (CHead c (Bind Abst) w) (lift (S O) O x0) x H5:ty3 g c u2 x0 ⇒
                         the thesis becomes P
                            (H_y) 
                               by (ty3_conv . . . . H5 . . H H1)
ty3 g c (THead (Bind Abst) w t) u2
                            end of H_y
                            (H_x) 
                               by (ty3_arity . . . . H0)

                                  ex2
                                    A
                                    λa1:A.arity g (CHead c (Bind Abst) w) t a1
                                    λa1:A.arity g (CHead c (Bind Abst) w) (lift (S O) O u2) (asucc g a1)
                            end of H_x
                            (H6) consider H_x
                            we proceed by induction on H6 to prove P
                               case ex_intro2 : x1:A H7:arity g (CHead c (Bind Abst) w) t x1 H8:arity g (CHead c (Bind Abst) w) (lift (S O) O u2) (asucc g x1) ⇒
                                  the thesis becomes P
                                     (H_x0) 
                                        by (ty3_arity . . . . H_y)

                                           ex2
                                             A
                                             λa1:A.arity g c (THead (Bind Abst) w t) a1
                                             λa1:A.arity g c u2 (asucc g a1)
                                     end of H_x0
                                     (H9) consider H_x0
                                     we proceed by induction on H9 to prove P
                                        case ex_intro2 : x2:A H10:arity g c (THead (Bind Abst) w t) x2 H11:arity g c u2 (asucc g x2) ⇒
                                           the thesis becomes P
                                              by (drop_refl .)
                                              we proved drop O O c c
                                              that is equivalent to drop (r (Bind Abst) O) O c c
                                              by (drop_drop . . . . previous .)
                                              we proved drop (S O) O (CHead c (Bind Abst) w) c
                                              by (arity_gen_lift . . . . . . H8 . previous)
                                              we proved arity g c u2 (asucc g x1)
                                              by (arity_mono . . . . previous . H11)
                                              we proved leq g (asucc g x1) (asucc g x2)
                                              by (asucc_inj . . . previous)
                                              we proved leq g x1 x2
                                              by (arity_repellent . . . . . H7 . H10 previous .)
P
P
P
P
          we proved P
       we proved 
          ∀g:G
            .∀c:C
              .∀w:T
                .∀t:T
                  .∀u1:T
                    .ty3 g c (THead (Bind Abst) w t) u1
                      →∀u2:T
                           .ty3 g (CHead c (Bind Abst) w) t (lift (S O) O u2)
                             →(pc3 c u1 u2)→∀P:Prop.P