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