DEFINITION sty0_ind()
TYPE =
       ∀g:G
         .∀P:C→T→T→Prop
           .∀c:C.∀n:nat.(P c (TSort n) (TSort (next g n)))
             →(∀c:C
                    .∀c1:C
                      .∀t:T
                        .∀n:nat
                          .getl n c (CHead c1 (Bind Abbr) t)
                            →∀t1:T.(sty0 g c1 t t1)→(P c1 t t1)→(P c (TLRef n) (lift (S n) O t1))
                  →(∀c:C
                         .∀c1:C
                           .∀t:T
                             .∀n:nat
                               .getl n c (CHead c1 (Bind Abst) t)
                                 →∀t1:T.(sty0 g c1 t t1)→(P c1 t t1)→(P c (TLRef n) (lift (S n) O t))
                       →(∀b:B
                              .∀c:C
                                .∀t:T
                                  .∀t1:T
                                    .∀t2:T
                                      .sty0 g (CHead c (Bind b) t) t1 t2
                                        →(P (CHead c (Bind b) t) t1 t2
                                             →P c (THead (Bind b) t t1) (THead (Bind b) t t2))
                            →(∀c:C
                                   .∀t:T
                                     .∀t1:T
                                       .∀t2:T
                                         .sty0 g c t1 t2
                                           →(P c t1 t2)→(P c (THead (Flat Appl) t t1) (THead (Flat Appl) t t2))
                                 →(∀c:C
                                        .∀t:T
                                          .∀t1:T
                                            .sty0 g c t t1
                                              →(P c t t1
                                                   →∀t2:T
                                                        .∀t3:T
                                                          .sty0 g c t2 t3
                                                            →(P c t2 t3)→(P c (THead (Flat Cast) t t2) (THead (Flat Cast) t1 t3)))
                                      →∀c:C.∀t:T.∀t1:T.(sty0 g c t t1)→(P c t t1))))))
BODY =
        assume g: G
        assume P: C→T→T→Prop
        suppose H: ∀c:C.∀n:nat.(P c (TSort n) (TSort (next g n)))
        suppose H1: 
           ∀c:C
             .∀c1:C
               .∀t:T
                 .∀n:nat
                   .getl n c (CHead c1 (Bind Abbr) t)
                     →∀t1:T.(sty0 g c1 t t1)→(P c1 t t1)→(P c (TLRef n) (lift (S n) O t1))
        suppose H2: 
           ∀c:C
             .∀c1:C
               .∀t:T
                 .∀n:nat
                   .getl n c (CHead c1 (Bind Abst) t)
                     →∀t1:T.(sty0 g c1 t t1)→(P c1 t t1)→(P c (TLRef n) (lift (S n) O t))
        suppose H3: 
           ∀b:B
             .∀c:C
               .∀t:T
                 .∀t1:T
                   .∀t2:T
                     .sty0 g (CHead c (Bind b) t) t1 t2
                       →(P (CHead c (Bind b) t) t1 t2
                            →P c (THead (Bind b) t t1) (THead (Bind b) t t2))
        suppose H4: 
           ∀c:C
             .∀t:T
               .∀t1:T
                 .∀t2:T
                   .sty0 g c t1 t2
                     →(P c t1 t2)→(P c (THead (Flat Appl) t t1) (THead (Flat Appl) t t2))
        suppose H5: 
           ∀c:C
             .∀t:T
               .∀t1:T
                 .sty0 g c t t1
                   →(P c t t1
                        →∀t2:T
                             .∀t3:T
                               .sty0 g c t2 t3
                                 →(P c t2 t3)→(P c (THead (Flat Cast) t t2) (THead (Flat Cast) t1 t3)))
          (aux) by well-founded reasoning we prove ∀c:C.∀t:T.∀t1:T.(sty0 g c t t1)→(P c t t1)
           assume c: C
           assume t: T
           assume t1: T
           suppose H6: sty0 g c t t1
             by cases on H6 we prove P c t t1
                case sty0_sort c1:C n:nat ⇒
                   the thesis becomes P c1 (TSort n) (TSort (next g n))
                   by (H . .)
P c1 (TSort n) (TSort (next g n))
                case sty0_abbr c1:C c2:C t2:T n:nat H7:getl n c1 (CHead c2 (Bind Abbr) t2) t3:T H8:sty0 g c2 t2 t3 ⇒
                   the thesis becomes P c1 (TLRef n) (lift (S n) O t3)
                   by (aux . . . H8)
                   we proved P c2 t2 t3
                   by (H1 . . . . H7 . H8 previous)
P c1 (TLRef n) (lift (S n) O t3)
                case sty0_abst c1:C c2:C t2:T n:nat H7:getl n c1 (CHead c2 (Bind Abst) t2) t3:T H8:sty0 g c2 t2 t3 ⇒
                   the thesis becomes P c1 (TLRef n) (lift (S n) O t2)
                   by (aux . . . H8)
                   we proved P c2 t2 t3
                   by (H2 . . . . H7 . H8 previous)
P c1 (TLRef n) (lift (S n) O t2)
                case sty0_bind b:B c1:C t2:T t3:T t4:T H7:sty0 g (CHead c1 (Bind b) t2) t3 t4 ⇒
                   the thesis becomes P c1 (THead (Bind b) t2 t3) (THead (Bind b) t2 t4)
                   by (aux . . . H7)
                   we proved P (CHead c1 (Bind b) t2) t3 t4
                   by (H3 . . . . . H7 previous)
P c1 (THead (Bind b) t2 t3) (THead (Bind b) t2 t4)
                case sty0_appl c1:C t2:T t3:T t4:T H7:sty0 g c1 t3 t4 ⇒
                   the thesis becomes P c1 (THead (Flat Appl) t2 t3) (THead (Flat Appl) t2 t4)
                   by (aux . . . H7)
                   we proved P c1 t3 t4
                   by (H4 . . . . H7 previous)
P c1 (THead (Flat Appl) t2 t3) (THead (Flat Appl) t2 t4)
                case sty0_cast c1:C t2:T t3:T H7:sty0 g c1 t2 t3 t4:T t5:T H8:sty0 g c1 t4 t5 ⇒
                   the thesis becomes P c1 (THead (Flat Cast) t2 t4) (THead (Flat Cast) t3 t5)
                   (h1) by (aux . . . H7) we proved P c1 t2 t3
                   (h2) by (aux . . . H8) we proved P c1 t4 t5
                   by (H5 . . . H7 h1 . . H8 h2)
P c1 (THead (Flat Cast) t2 t4) (THead (Flat Cast) t3 t5)
             we proved P c t t1
∀c:C.∀t:T.∀t1:T.(sty0 g c t t1)→(P c t t1)
          done
          consider aux
          we proved ∀c:C.∀t:T.∀t1:T.(sty0 g c t t1)→(P c t t1)
       we proved 
          ∀g:G
            .∀P:C→T→T→Prop
              .∀c:C.∀n:nat.(P c (TSort n) (TSort (next g n)))
                →(∀c:C
                       .∀c1:C
                         .∀t:T
                           .∀n:nat
                             .getl n c (CHead c1 (Bind Abbr) t)
                               →∀t1:T.(sty0 g c1 t t1)→(P c1 t t1)→(P c (TLRef n) (lift (S n) O t1))
                     →(∀c:C
                            .∀c1:C
                              .∀t:T
                                .∀n:nat
                                  .getl n c (CHead c1 (Bind Abst) t)
                                    →∀t1:T.(sty0 g c1 t t1)→(P c1 t t1)→(P c (TLRef n) (lift (S n) O t))
                          →(∀b:B
                                 .∀c:C
                                   .∀t:T
                                     .∀t1:T
                                       .∀t2:T
                                         .sty0 g (CHead c (Bind b) t) t1 t2
                                           →(P (CHead c (Bind b) t) t1 t2
                                                →P c (THead (Bind b) t t1) (THead (Bind b) t t2))
                               →(∀c:C
                                      .∀t:T
                                        .∀t1:T
                                          .∀t2:T
                                            .sty0 g c t1 t2
                                              →(P c t1 t2)→(P c (THead (Flat Appl) t t1) (THead (Flat Appl) t t2))
                                    →(∀c:C
                                           .∀t:T
                                             .∀t1:T
                                               .sty0 g c t t1
                                                 →(P c t t1
                                                      →∀t2:T
                                                           .∀t3:T
                                                             .sty0 g c t2 t3
                                                               →(P c t2 t3)→(P c (THead (Flat Cast) t t2) (THead (Flat Cast) t1 t3)))
                                         →∀c:C.∀t:T.∀t1:T.(sty0 g c t t1)→(P c t t1))))))