DEFINITION C_ind()
TYPE =
       ∀P:C→Prop
         .∀n:nat.(P (CSort n))
           →(∀c:C.(P c)→∀k:K.∀t:T.(P (CHead c k t)))→∀c:C.(P c)
BODY =
        assume P: C→Prop
        suppose H: ∀n:nat.(P (CSort n))
        suppose H1: ∀c:C.(P c)→∀k:K.∀t:T.(P (CHead c k t))
          (aux) by well-founded reasoning we prove ∀c:C.(P c)
          assume c: C
             by cases on c we prove P c
                case CSort n:nat ⇒
                   the thesis becomes P (CSort n)
                   by (H .)
P (CSort n)
                case CHead c1:C k:K t:T ⇒
                   the thesis becomes P (CHead c1 k t)
                   by (aux .)
                   we proved P c1
                   by (H1 . previous . .)
P (CHead c1 k t)
             we proved P c
∀c:C.(P c)
          done
          consider aux
          we proved ∀c:C.(P c)
       we proved 
          ∀P:C→Prop
            .∀n:nat.(P (CSort n))
              →(∀c:C.(P c)→∀k:K.∀t:T.(P (CHead c k t)))→∀c:C.(P c)