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 =
Show proof