DEFINITION c_tail_ind()
TYPE =
       ∀P:C→Prop
         .∀n:nat.(P (CSort n))
           →(∀c:C.(P c)→∀k:K.∀t:T.(P (CTail k t c)))→∀c:C.(P c)
BODY =
        assume P: C→Prop
        suppose H: ∀n:nat.(P (CSort n))
        suppose H0: ∀c:C.(P c)→∀k:K.∀t:T.(P (CTail k t c))
        assume c: C
          assume c0: C
             we proceed by induction on c0 to prove (∀d:C.(clt d c0)→(P d))→(P c0)
                case CSort : n:nat ⇒
                   the thesis becomes (∀d:C.(clt d (CSort n))→(P d))→(P (CSort n))
                      suppose : ∀d:C.(clt d (CSort n))→(P d)
                         by (H .)
                         we proved P (CSort n)
(∀d:C.(clt d (CSort n))→(P d))→(P (CSort n))
                case CHead : c1:C k:K t:T ⇒
                   the thesis becomes ∀H2:∀d:C.(clt d (CHead c1 k t))→(P d).(P (CHead c1 k t))
                   () by induction hypothesis we know (∀d:C.(clt d c1)→(P d))→(P c1)
                      suppose H2: ∀d:C.(clt d (CHead c1 k t))→(P d)
                         (H_x) 
                            by (chead_ctail . . .)
ex_3 K C T λh:K.λd:C.λu:T.eq C (CHead c1 k t) (CTail h u d)
                         end of H_x
                         (H3) consider H_x
                         we proceed by induction on H3 to prove P (CHead c1 k t)
                            case ex_3_intro : x0:K x1:C x2:T H4:eq C (CHead c1 k t) (CTail x0 x2 x1) ⇒
                               the thesis becomes P (CHead c1 k t)
                                  (H5) 
                                     we proceed by induction on H4 to prove ∀d:C.(clt d (CTail x0 x2 x1))→(P d)
                                        case refl_equal : ⇒
                                           the thesis becomes the hypothesis H2
∀d:C.(clt d (CTail x0 x2 x1))→(P d)
                                  end of H5
                                  by (clt_thead . . .)
                                  we proved clt x1 (CTail x0 x2 x1)
                                  by (H5 . previous)
                                  we proved P x1
                                  by (H0 . previous . .)
                                  we proved P (CTail x0 x2 x1)
                                  by (eq_ind_r . . . previous . H4)
P (CHead c1 k t)
                         we proved P (CHead c1 k t)
∀H2:∀d:C.(clt d (CHead c1 k t))→(P d).(P (CHead c1 k t))
             we proved (∀d:C.(clt d c0)→(P d))→(P c0)
          we proved ∀c0:C.(∀d:C.(clt d c0)→(P d))→(P c0)
          by (clt_wf_ind . previous .)
          we proved P c
       we proved 
          ∀P:C→Prop
            .∀n:nat.(P (CSort n))
              →(∀c:C.(P c)→∀k:K.∀t:T.(P (CTail k t c)))→∀c:C.(P c)