DEFINITION wf3_total()
TYPE =
       ∀g:G.∀c1:C.(ex C λc2:C.wf3 g c1 c2)
BODY =
        assume g: G
        assume c1: C
          we proceed by induction on c1 to prove ex C λc2:C.wf3 g c1 c2
             case CSort : n:nat ⇒
                the thesis becomes ex C λc2:C.wf3 g (CSort n) c2
                   by (wf3_sort . .)
                   we proved wf3 g (CSort n) (CSort n)
                   by (ex_intro . . . previous)
ex C λc2:C.wf3 g (CSort n) c2
             case CHead : c:C k:K t:T ⇒
                the thesis becomes ex C λc2:C.wf3 g (CHead c k t) c2
                (H) by induction hypothesis we know ex C λc2:C.wf3 g c c2
                   (H0) consider H
                   we proceed by induction on H0 to prove ex C λc2:C.wf3 g (CHead c k t) c2
                      case ex_intro : x:C H1:wf3 g c x ⇒
                         the thesis becomes ex C λc2:C.wf3 g (CHead c k t) c2
                            we proceed by induction on k to prove ex C λc2:C.wf3 g (CHead c k t) c2
                               case Bind : b:B ⇒
                                  the thesis becomes ex C λc2:C.wf3 g (CHead c (Bind b) t) c2
                                     (H_x) 
                                        by (ty3_inference . . .)
or (ex T λt2:T.ty3 g c t t2) ∀t2:T.(ty3 g c t t2)→False
                                     end of H_x
                                     (H2) consider H_x
                                     we proceed by induction on H2 to prove ex C λc2:C.wf3 g (CHead c (Bind b) t) c2
                                        case or_introl : H3:ex T λt2:T.ty3 g c t t2 ⇒
                                           the thesis becomes ex C λc2:C.wf3 g (CHead c (Bind b) t) c2
                                              we proceed by induction on H3 to prove ex C λc2:C.wf3 g (CHead c (Bind b) t) c2
                                                 case ex_intro : x0:T H4:ty3 g c t x0 ⇒
                                                    the thesis becomes ex C λc2:C.wf3 g (CHead c (Bind b) t) c2
                                                       by (wf3_bind . . . H1 . . H4 .)
                                                       we proved wf3 g (CHead c (Bind b) t) (CHead x (Bind b) t)
                                                       by (ex_intro . . . previous)
ex C λc2:C.wf3 g (CHead c (Bind b) t) c2
ex C λc2:C.wf3 g (CHead c (Bind b) t) c2
                                        case or_intror : H3:∀t2:T.(ty3 g c t t2)→False ⇒
                                           the thesis becomes ex C λc2:C.wf3 g (CHead c (Bind b) t) c2
                                              by (wf3_void . . . H1 . H3 .)
                                              we proved wf3 g (CHead c (Bind b) t) (CHead x (Bind Void) (TSort O))
                                              by (ex_intro . . . previous)
ex C λc2:C.wf3 g (CHead c (Bind b) t) c2
ex C λc2:C.wf3 g (CHead c (Bind b) t) c2
                               case Flat : f:F ⇒
                                  the thesis becomes ex C λc2:C.wf3 g (CHead c (Flat f) t) c2
                                     by (wf3_flat . . . H1 . .)
                                     we proved wf3 g (CHead c (Flat f) t) x
                                     by (ex_intro . . . previous)
ex C λc2:C.wf3 g (CHead c (Flat f) t) c2
ex C λc2:C.wf3 g (CHead c k t) c2
ex C λc2:C.wf3 g (CHead c k t) c2
          we proved ex C λc2:C.wf3 g c1 c2
       we proved ∀g:G.∀c1:C.(ex C λc2:C.wf3 g c1 c2)