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