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 =
Show proof