DEFINITION csubt_ind()
TYPE =
       ∀g:G
         .∀P:C→C→Prop
           .∀n:nat.(P (CSort n) (CSort n))
             →(∀c:C
                    .∀c1:C.(csubt g c c1)→(P c c1)→∀k:K.∀t:T.(P (CHead c k t) (CHead c1 k t))
                  →(∀c:C
                         .∀c1:C
                           .csubt 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
                                .csubt g c c1
                                  →(P c c1
                                       →∀t:T
                                            .∀t1:T
                                              .ty3 g c t t1
                                                →(ty3 g c1 t t1)→(P (CHead c (Bind Abst) t1) (CHead c1 (Bind Abbr) t)))
                            →∀c:C.∀c1:C.(csubt g c c1)→(P c c1))))
BODY =
Show proof