DEFINITION ty3_ind()
TYPE =
       ∀g:G
         .∀P:C→T→T→Prop
           .∀c:C
               .∀t:T
                 .∀t1:T
                   .ty3 g c t t1
                     →(P c t t1)→∀t2:T.∀t3:T.(ty3 g c t2 t3)→(P c t2 t3)→(pc3 c t3 t)→(P c t2 t)
             →(∀c:C.∀n:nat.(P c (TSort n) (TSort (next g n)))
                  →(∀n:nat
                         .∀c:C
                           .∀c1:C
                             .∀t:T
                               .getl n c (CHead c1 (Bind Abbr) t)
                                 →∀t1:T.(ty3 g c1 t t1)→(P c1 t t1)→(P c (TLRef n) (lift (S n) O t1))
                       →(∀n:nat
                              .∀c:C
                                .∀c1:C
                                  .∀t:T
                                    .getl n c (CHead c1 (Bind Abst) t)
                                      →∀t1:T.(ty3 g c1 t t1)→(P c1 t t1)→(P c (TLRef n) (lift (S n) O t))
                            →(∀c:C
                                   .∀t:T
                                     .∀t1:T
                                       .ty3 g c t t1
                                         →(P c t t1
                                              →∀b:B
                                                   .∀t2:T
                                                     .∀t3:T
                                                       .ty3 g (CHead c (Bind b) t) t2 t3
                                                         →(P (CHead c (Bind b) t) t2 t3
                                                              →P c (THead (Bind b) t t2) (THead (Bind b) t t3)))
                                 →(∀c:C
                                        .∀t:T
                                          .∀t1:T
                                            .ty3 g c t t1
                                              →(P c t t1
                                                   →∀t2:T
                                                        .∀t3:T
                                                          .ty3 g c t2 (THead (Bind Abst) t1 t3)
                                                            →(P c t2 (THead (Bind Abst) t1 t3)
                                                                 →(P
                                                                      c
                                                                      THead (Flat Appl) t t2
                                                                      THead (Flat Appl) t (THead (Bind Abst) t1 t3))))
                                      →(∀c:C
                                             .∀t:T
                                               .∀t1:T
                                                 .ty3 g c t t1
                                                   →(P c t t1
                                                        →∀t2:T
                                                             .ty3 g c t1 t2
                                                               →(P c t1 t2)→(P c (THead (Flat Cast) t1 t) (THead (Flat Cast) t2 t1)))
                                           →∀c:C.∀t:T.∀t1:T.(ty3 g c t t1)→(P c t t1)))))))
BODY =
Show proof