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