DEFINITION C_rec()
TYPE =
       ΠP:C→Set
         .Π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