DEFINITION wf3_ind()
TYPE =
       ∀g:G
         .∀P:C→C→Prop
           .∀n:nat.(P (CSort n) (CSort n))
             →(∀c:C
                    .∀c1:C
                      .wf3 g c c1
                        →(P c c1
                             →∀t:T.∀t1:T.(ty3 g c t t1)→∀b:B.(P (CHead c (Bind b) t) (CHead c1 (Bind b) t)))
                  →(∀c:C
                         .∀c1:C
                           .wf3 g c c1
                             →(P c c1
                                  →∀t:T
                                       .∀t:T.(ty3 g c t t)→False
                                         →∀b:B.(P (CHead c (Bind b) t) (CHead c1 (Bind Void) (TSort O))))
                       →(∀c:C.∀c1:C.(wf3 g c c1)→(P c c1)→∀t:T.∀f:F.(P (CHead c (Flat f) t) c1)
                            →∀c:C.∀c1:C.(wf3 g c c1)→(P c c1))))
BODY =
        assume g: G
        assume P: C→C→Prop
        suppose H: ∀n:nat.(P (CSort n) (CSort n))
        suppose H1: 
           ∀c:C
             .∀c1:C
               .wf3 g c c1
                 →(P c c1
                      →∀t:T.∀t1:T.(ty3 g c t t1)→∀b:B.(P (CHead c (Bind b) t) (CHead c1 (Bind b) t)))
        suppose H2: 
           ∀c:C
             .∀c1:C
               .wf3 g c c1
                 →(P c c1
                      →∀t:T
                           .∀t:T.(ty3 g c t t)→False
                             →∀b:B.(P (CHead c (Bind b) t) (CHead c1 (Bind Void) (TSort O))))
        suppose H3: ∀c:C.∀c1:C.(wf3 g c c1)→(P c c1)→∀t:T.∀f:F.(P (CHead c (Flat f) t) c1)
          (aux) by well-founded reasoning we prove ∀c:C.∀c1:C.(wf3 g c c1)→(P c c1)
           assume c: C
           assume c1: C
           suppose H4: wf3 g c c1
             by cases on H4 we prove P c c1
                case wf3_sort n:nat ⇒
                   the thesis becomes P (CSort n) (CSort n)
                   by (H .)
P (CSort n) (CSort n)
                case wf3_bind c2:C c3:C H5:wf3 g c2 c3 t:T t1:T H6:ty3 g c2 t t1 b:B ⇒
                   the thesis becomes P (CHead c2 (Bind b) t) (CHead c3 (Bind b) t)
                   by (aux . . H5)
                   we proved P c2 c3
                   by (H1 . . H5 previous . . H6 .)
P (CHead c2 (Bind b) t) (CHead c3 (Bind b) t)
                case wf3_void c2:C c3:C H5:wf3 g c2 c3 t:T H6:∀t:T.(ty3 g c2 t t)→False b:B ⇒
                   the thesis becomes P (CHead c2 (Bind b) t) (CHead c3 (Bind Void) (TSort O))
                   by (aux . . H5)
                   we proved P c2 c3
                   by (H2 . . H5 previous . H6 .)
P (CHead c2 (Bind b) t) (CHead c3 (Bind Void) (TSort O))
                case wf3_flat c2:C c3:C H5:wf3 g c2 c3 t:T f:F ⇒
                   the thesis becomes P (CHead c2 (Flat f) t) c3
                   by (aux . . H5)
                   we proved P c2 c3
                   by (H3 . . H5 previous . .)
P (CHead c2 (Flat f) t) c3
             we proved P c c1
∀c:C.∀c1:C.(wf3 g c c1)→(P c c1)
          done
          consider aux
          we proved ∀c:C.∀c1:C.(wf3 g c c1)→(P c c1)
       we proved 
          ∀g:G
            .∀P:C→C→Prop
              .∀n:nat.(P (CSort n) (CSort n))
                →(∀c:C
                       .∀c1:C
                         .wf3 g c c1
                           →(P c c1
                                →∀t:T.∀t1:T.(ty3 g c t t1)→∀b:B.(P (CHead c (Bind b) t) (CHead c1 (Bind b) t)))
                     →(∀c:C
                            .∀c1:C
                              .wf3 g c c1
                                →(P c c1
                                     →∀t:T
                                          .∀t:T.(ty3 g c t t)→False
                                            →∀b:B.(P (CHead c (Bind b) t) (CHead c1 (Bind Void) (TSort O))))
                          →(∀c:C.∀c1:C.(wf3 g c c1)→(P c c1)→∀t:T.∀f:F.(P (CHead c (Flat f) t) c1)
                               →∀c:C.∀c1:C.(wf3 g c c1)→(P c c1))))