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 =
λP:C→Set
         .λf:Πn:nat.(P (CSort n))
           .λf1:Πc:C.(P c)→Πk:K.Πt:T.(P (CHead c k t))
             .FIXaux{
               aux:Πc:C.(P c)
               :=λc:C.<P> CASE c OF CSort n⇒f n | CHead c1 k t⇒f1 c1 (aux c1) k t
               }