DEFINITION ex2_arity()
TYPE =
       ∀g:G.∀a:A.(arity g ex2_c ex2_t a)→∀P:Prop.P
BODY =
        assume g: G
        assume a: A
          we must prove (arity g ex2_c ex2_t a)→∀P:Prop.P
          or equivalently 
                (arity
                    g
                    CSort O
                    THead (Flat Appl) (TSort O) (TSort O)
                    a)
                  →∀P:Prop.P
           suppose H: 
              arity
                g
                CSort O
                THead (Flat Appl) (TSort O) (TSort O)
                a
           assume P: Prop
             (H0) 
                by (arity_gen_appl . . . . . H)

                   ex2
                     A
                     λa1:A.arity g (CSort O) (TSort O) a1
                     λa1:A.arity g (CSort O) (TSort O) (AHead a1 a)
             end of H0
             we proceed by induction on H0 to prove P
                case ex_intro2 : x:A :arity g (CSort O) (TSort O) x H2:arity g (CSort O) (TSort O) (AHead x a) ⇒
                   the thesis becomes P
                      (H_x) 
                         by (arity_gen_sort . . . . H2)
                         we proved leq g (AHead x a) (ASort O O)
                         by (leq_gen_head1 . . . . previous)
ex3_2 A A λa3:A.λ:A.leq g x a3 λ:A.λa4:A.leq g a a4 λa3:A.λa4:A.eq A (ASort O O) (AHead a3 a4)
                      end of H_x
                      (H3) consider H_x
                      we proceed by induction on H3 to prove P
                         case ex3_2_intro : x0:A x1:A :leq g x x0 :leq g a x1 H6:eq A (ASort O O) (AHead x0 x1) ⇒
                            the thesis becomes P
                               (H7) 
                                  we proceed by induction on H6 to prove <λ:A.Prop> CASE AHead x0 x1 OF ASort  ⇒True | AHead  ⇒False
                                     case refl_equal : ⇒
                                        the thesis becomes <λ:A.Prop> CASE ASort O O OF ASort  ⇒True | AHead  ⇒False
                                           consider I
                                           we proved True
<λ:A.Prop> CASE ASort O O OF ASort  ⇒True | AHead  ⇒False
<λ:A.Prop> CASE AHead x0 x1 OF ASort  ⇒True | AHead  ⇒False
                               end of H7
                               consider H7
                               we proved <λ:A.Prop> CASE AHead x0 x1 OF ASort  ⇒True | AHead  ⇒False
                               that is equivalent to False
                               we proceed by induction on the previous result to prove P
P
P
             we proved P
          we proved 
             (arity
                 g
                 CSort O
                 THead (Flat Appl) (TSort O) (TSort O)
                 a)
               →∀P:Prop.P
          that is equivalent to (arity g ex2_c ex2_t a)→∀P:Prop.P
       we proved ∀g:G.∀a:A.(arity g ex2_c ex2_t a)→∀P:Prop.P