DEFINITION arity_gen_appls()
TYPE =
       ∀g:G
         .∀c:C
           .∀t:T
             .∀vs:TList
               .∀a2:A
                 .arity g c (THeads (Flat Appl) vs t) a2
                   →ex A λa:A.arity g c t a
BODY =
        assume g: G
        assume c: C
        assume t: T
        assume vs: TList
          we proceed by induction on vs to prove 
             ∀a2:A
               .arity g c (THeads (Flat Appl) vs t) a2
                 →ex A λa:A.arity g c t a
             case TNil : ⇒
                the thesis becomes 
                ∀a2:A
                  .arity g c (THeads (Flat Appl) TNil t) a2
                    →ex A λa:A.arity g c t a
                   assume a2: A
                      we must prove 
                            arity g c (THeads (Flat Appl) TNil t) a2
                              →ex A λa:A.arity g c t a
                      or equivalently (arity g c t a2)→(ex A λa:A.arity g c t a)
                      suppose H: arity g c t a2
                         by (ex_intro . . . H)
                         we proved ex A λa:A.arity g c t a
                      we proved (arity g c t a2)→(ex A λa:A.arity g c t a)
                      that is equivalent to 
                         arity g c (THeads (Flat Appl) TNil t) a2
                           →ex A λa:A.arity g c t a

                      ∀a2:A
                        .arity g c (THeads (Flat Appl) TNil t) a2
                          →ex A λa:A.arity g c t a
             case TCons : t0:T t1:TList ⇒
                the thesis becomes 
                ∀a2:A
                  .arity g c (THeads (Flat Appl) (TCons t0 t1) t) a2
                    →ex A λa:A.arity g c t a
                (H) by induction hypothesis we know 
                   ∀a2:A
                     .arity g c (THeads (Flat Appl) t1 t) a2
                       →ex A λa:A.arity g c t a
                   assume a2: A
                      we must prove 
                            arity g c (THeads (Flat Appl) (TCons t0 t1) t) a2
                              →ex A λa:A.arity g c t a
                      or equivalently 
                            arity g c (THead (Flat Appl) t0 (THeads (Flat Appl) t1 t)) a2
                              →ex A λa:A.arity g c t a
                      suppose H0: arity g c (THead (Flat Appl) t0 (THeads (Flat Appl) t1 t)) a2
                         (H1) 
                            by (arity_gen_appl . . . . . H0)

                               ex2 A λa1:A.arity g c t0 a1 λa1:A.arity g c (THeads (Flat Appl) t1 t) (AHead a1 a2)
                         end of H1
                         we proceed by induction on H1 to prove ex A λa:A.arity g c t a
                            case ex_intro2 : x:A :arity g c t0 x H3:arity g c (THeads (Flat Appl) t1 t) (AHead x a2) ⇒
                               the thesis becomes ex A λa:A.arity g c t a
                                  (H_x) 
                                     by (H . H3)
ex A λa:A.arity g c t a
                                  end of H_x
                                  (H4) consider H_x
                                  we proceed by induction on H4 to prove ex A λa:A.arity g c t a
                                     case ex_intro : x0:A H5:arity g c t x0 ⇒
                                        the thesis becomes ex A λa:A.arity g c t a
                                           by (ex_intro . . . H5)
ex A λa:A.arity g c t a
ex A λa:A.arity g c t a
                         we proved ex A λa:A.arity g c t a
                      we proved 
                         arity g c (THead (Flat Appl) t0 (THeads (Flat Appl) t1 t)) a2
                           →ex A λa:A.arity g c t a
                      that is equivalent to 
                         arity g c (THeads (Flat Appl) (TCons t0 t1) t) a2
                           →ex A λa:A.arity g c t a

                      ∀a2:A
                        .arity g c (THeads (Flat Appl) (TCons t0 t1) t) a2
                          →ex A λa:A.arity g c t a
          we proved 
             ∀a2:A
               .arity g c (THeads (Flat Appl) vs t) a2
                 →ex A λa:A.arity g c t a
       we proved 
          ∀g:G
            .∀c:C
              .∀t:T
                .∀vs:TList
                  .∀a2:A
                    .arity g c (THeads (Flat Appl) vs t) a2
                      →ex A λa:A.arity g c t a