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