DEFINITION csuba_ind()
TYPE =
       ∀g:G
         .∀P:C→C→Prop
           .∀n:nat.(P (CSort n) (CSort n))
             →(∀c:C
                    .∀c1:C.(csuba g c c1)→(P c c1)→∀k:K.∀t:T.(P (CHead c k t) (CHead c1 k t))
                  →(∀c:C
                         .∀c1:C
                           .csuba g c c1
                             →(P c c1
                                  →∀b:B
                                       .not (eq B b Void)
                                         →∀t:T.∀t1:T.(P (CHead c (Bind Void) t) (CHead c1 (Bind b) t1)))
                       →(∀c:C
                              .∀c1:C
                                .csuba g c c1
                                  →(P c c1
                                       →∀t:T
                                            .∀a:A
                                              .arity g c t (asucc g a)
                                                →∀t1:T
                                                     .arity g c1 t1 a
                                                       →P (CHead c (Bind Abst) t) (CHead c1 (Bind Abbr) t1))
                            →∀c:C.∀c1:C.(csuba g c c1)→(P c c1))))
BODY =
        assume g: G
        assume P: C→C→Prop
        suppose H: ∀n:nat.(P (CSort n) (CSort n))
        suppose H1: 
           ∀c:C
             .∀c1:C.(csuba g c c1)→(P c c1)→∀k:K.∀t:T.(P (CHead c k t) (CHead c1 k t))
        suppose H2: 
           ∀c:C
             .∀c1:C
               .csuba g c c1
                 →(P c c1
                      →∀b:B
                           .not (eq B b Void)
                             →∀t:T.∀t1:T.(P (CHead c (Bind Void) t) (CHead c1 (Bind b) t1)))
        suppose H3: 
           ∀c:C
             .∀c1:C
               .csuba g c c1
                 →(P c c1
                      →∀t:T
                           .∀a:A
                             .arity g c t (asucc g a)
                               →∀t1:T
                                    .arity g c1 t1 a
                                      →P (CHead c (Bind Abst) t) (CHead c1 (Bind Abbr) t1))
          (aux) by well-founded reasoning we prove ∀c:C.∀c1:C.(csuba g c c1)→(P c c1)
           assume c: C
           assume c1: C
           suppose H4: csuba g c c1
             by cases on H4 we prove P c c1
                case csuba_sort n:nat ⇒
                   the thesis becomes P (CSort n) (CSort n)
                   by (H .)
P (CSort n) (CSort n)
                case csuba_head c2:C c3:C H5:csuba g c2 c3 k:K t:T ⇒
                   the thesis becomes P (CHead c2 k t) (CHead c3 k t)
                   by (aux . . H5)
                   we proved P c2 c3
                   by (H1 . . H5 previous . .)
P (CHead c2 k t) (CHead c3 k t)
                case csuba_void c2:C c3:C H5:csuba g c2 c3 b:B H6:not (eq B b Void) t:T t1:T ⇒
                   the thesis becomes P (CHead c2 (Bind Void) t) (CHead c3 (Bind b) t1)
                   by (aux . . H5)
                   we proved P c2 c3
                   by (H2 . . H5 previous . H6 . .)
P (CHead c2 (Bind Void) t) (CHead c3 (Bind b) t1)
                case csuba_abst c2:C c3:C H5:csuba g c2 c3 t:T a:A H6:arity g c2 t (asucc g a) t1:T H7:arity g c3 t1 a ⇒
                   the thesis becomes P (CHead c2 (Bind Abst) t) (CHead c3 (Bind Abbr) t1)
                   by (aux . . H5)
                   we proved P c2 c3
                   by (H3 . . H5 previous . . H6 . H7)
P (CHead c2 (Bind Abst) t) (CHead c3 (Bind Abbr) t1)
             we proved P c c1
∀c:C.∀c1:C.(csuba g c c1)→(P c c1)
          done
          consider aux
          we proved ∀c:C.∀c1:C.(csuba g c c1)→(P c c1)
       we proved 
          ∀g:G
            .∀P:C→C→Prop
              .∀n:nat.(P (CSort n) (CSort n))
                →(∀c:C
                       .∀c1:C.(csuba g c c1)→(P c c1)→∀k:K.∀t:T.(P (CHead c k t) (CHead c1 k t))
                     →(∀c:C
                            .∀c1:C
                              .csuba g c c1
                                →(P c c1
                                     →∀b:B
                                          .not (eq B b Void)
                                            →∀t:T.∀t1:T.(P (CHead c (Bind Void) t) (CHead c1 (Bind b) t1)))
                          →(∀c:C
                                 .∀c1:C
                                   .csuba g c c1
                                     →(P c c1
                                          →∀t:T
                                               .∀a:A
                                                 .arity g c t (asucc g a)
                                                   →∀t1:T
                                                        .arity g c1 t1 a
                                                          →P (CHead c (Bind Abst) t) (CHead c1 (Bind Abbr) t1))
                               →∀c:C.∀c1:C.(csuba g c c1)→(P c c1))))