DEFINITION csubv_ind()
TYPE =
       ∀P:C→C→Prop
         .∀n:nat.(P (CSort n) (CSort n))
           →(∀c:C
                  .∀c1:C
                    .csubv c c1
                      →(P c c1
                           →∀t:T.∀t1:T.(P (CHead c (Bind Void) t) (CHead c1 (Bind Void) t1)))
                →(∀c:C
                       .∀c1:C
                         .csubv c c1
                           →(P c c1
                                →∀b:B
                                     .not (eq B b Void)
                                       →∀b1:B.∀t:T.∀t1:T.(P (CHead c (Bind b) t) (CHead c1 (Bind b1) t1)))
                     →(∀c:C
                            .∀c1:C
                              .csubv c c1
                                →(P c c1)→∀f:F.∀f1:F.∀t:T.∀t1:T.(P (CHead c (Flat f) t) (CHead c1 (Flat f1) t1))
                          →∀c:C.∀c1:C.(csubv c c1)→(P c c1))))
BODY =
Show proof