DEFINITION arity_repellent()
TYPE =
       ∀g:G
         .∀c:C
           .∀w:T
             .∀t:T
               .∀a1:A
                 .arity g (CHead c (Bind Abst) w) t a1
                   →∀a2:A.(arity g c (THead (Bind Abst) w t) a2)→(leq g a1 a2)→∀P:Prop.P
BODY =
        assume g: G
        assume c: C
        assume w: T
        assume t: T
        assume a1: A
        suppose H: arity g (CHead c (Bind Abst) w) t a1
        assume a2: A
        suppose H0: arity g c (THead (Bind Abst) w t) a2
        suppose H1: leq g a1 a2
        assume P: Prop
          (H_y) 
             by (arity_repl . . . . H . H1)
arity g (CHead c (Bind Abst) w) t a2
          end of H_y
          (H2) 
             by (arity_gen_abst . . . . . H0)

                ex3_2
                  A
                  A
                  λa1:A.λa2:A.eq A a2 (AHead a1 a2)
                  λa1:A.λ:A.arity g c w (asucc g a1)
                  λ:A.λa2:A.arity g (CHead c (Bind Abst) w) t a2
          end of H2
          we proceed by induction on H2 to prove P
             case ex3_2_intro : x0:A x1:A H3:eq A a2 (AHead x0 x1) :arity g c w (asucc g x0) H5:arity g (CHead c (Bind Abst) w) t x1 ⇒
                the thesis becomes P
                   (H6) 
                      we proceed by induction on H3 to prove arity g (CHead c (Bind Abst) w) t (AHead x0 x1)
                         case refl_equal : ⇒
                            the thesis becomes the hypothesis H_y
arity g (CHead c (Bind Abst) w) t (AHead x0 x1)
                   end of H6
                   by (arity_mono . . . . H6 . H5)
                   we proved leq g (AHead x0 x1) x1
                   by (leq_ahead_false_2 . . . previous .)
P
          we proved P
       we proved 
          ∀g:G
            .∀c:C
              .∀w:T
                .∀t:T
                  .∀a1:A
                    .arity g (CHead c (Bind Abst) w) t a1
                      →∀a2:A.(arity g c (THead (Bind Abst) w t) a2)→(leq g a1 a2)→∀P:Prop.P