DEFINITION pr0_ind()
TYPE =
       ∀P:T→T→Prop
         .∀t:T.(P t t)
           →(∀t:T
                  .∀t1:T
                    .pr0 t t1
                      →(P t t1)→∀t2:T.∀t3:T.(pr0 t2 t3)→(P t2 t3)→∀k:K.(P (THead k t t2) (THead k t1 t3))
                →(∀t:T
                       .∀t1:T
                         .∀t2:T
                           .pr0 t1 t2
                             →(P t1 t2
                                  →∀t3:T
                                       .∀t4:T
                                         .pr0 t3 t4
                                           →(P t3 t4
                                                →(P
                                                     THead (Flat Appl) t1 (THead (Bind Abst) t t3)
                                                     THead (Bind Abbr) t2 t4)))
                     →(∀b:B
                            .not (eq B b Abst)
                              →∀t:T
                                   .∀t1:T
                                     .pr0 t t1
                                       →(P t t1
                                            →∀t2:T
                                                 .∀t3:T
                                                   .pr0 t2 t3
                                                     →(P t2 t3
                                                          →∀t4:T
                                                               .∀t5:T
                                                                 .pr0 t4 t5
                                                                   →(P t4 t5
                                                                        →(P
                                                                             THead (Flat Appl) t (THead (Bind b) t2 t4)
                                                                             THead (Bind b) t3 (THead (Flat Appl) (lift (S O) O t1) t5)))))
                          →(∀t:T
                                 .∀t1:T
                                   .pr0 t t1
                                     →(P t t1
                                          →∀t2:T
                                               .∀t3:T
                                                 .pr0 t2 t3
                                                   →(P t2 t3
                                                        →∀t4:T.(subst0 O t1 t3 t4)→(P (THead (Bind Abbr) t t2) (THead (Bind Abbr) t1 t4))))
                               →(∀b:B
                                      .not (eq B b Abst)
                                        →∀t:T
                                             .∀t1:T.(pr0 t t1)→(P t t1)→∀t2:T.(P (THead (Bind b) t2 (lift (S O) O t)) t1)
                                    →(∀t:T.∀t1:T.(pr0 t t1)→(P t t1)→∀t2:T.(P (THead (Flat Cast) t2 t) t1)
                                         →∀t:T.∀t1:T.(pr0 t t1)→(P t t1)))))))
BODY =
Show proof