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 =
        assume P: C→C→Prop
        suppose H: ∀n:nat.(P (CSort n) (CSort n))
        suppose H1: 
           ∀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)))
        suppose H2: 
           ∀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)))
        suppose H3: 
           ∀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))
          (aux) by well-founded reasoning we prove ∀c:C.∀c1:C.(csubv c c1)→(P c c1)
           assume c: C
           assume c1: C
           suppose H4: csubv c c1
             by cases on H4 we prove P c c1
                case csubv_sort n:nat ⇒
                   the thesis becomes P (CSort n) (CSort n)
                   by (H .)
P (CSort n) (CSort n)
                case csubv_void c2:C c3:C H5:csubv c2 c3 t:T t1:T ⇒
                   the thesis becomes P (CHead c2 (Bind Void) t) (CHead c3 (Bind Void) t1)
                   by (aux . . H5)
                   we proved P c2 c3
                   by (H1 . . H5 previous . .)
P (CHead c2 (Bind Void) t) (CHead c3 (Bind Void) t1)
                case csubv_bind c2:C c3:C H5:csubv c2 c3 b:B H6:not (eq B b Void) b1:B t:T t1:T ⇒
                   the thesis becomes P (CHead c2 (Bind b) t) (CHead c3 (Bind b1) t1)
                   by (aux . . H5)
                   we proved P c2 c3
                   by (H2 . . H5 previous . H6 . . .)
P (CHead c2 (Bind b) t) (CHead c3 (Bind b1) t1)
                case csubv_flat c2:C c3:C H5:csubv c2 c3 f:F f1:F t:T t1:T ⇒
                   the thesis becomes P (CHead c2 (Flat f) t) (CHead c3 (Flat f1) t1)
                   by (aux . . H5)
                   we proved P c2 c3
                   by (H3 . . H5 previous . . . .)
P (CHead c2 (Flat f) t) (CHead c3 (Flat f1) t1)
             we proved P c c1
∀c:C.∀c1:C.(csubv c c1)→(P c c1)
          done
          consider aux
          we proved ∀c:C.∀c1:C.(csubv c c1)→(P c c1)
       we proved 
          ∀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))))