DEFINITION C_rect()
TYPE =
       ΠP:C
                →(Type:93192:cic:/matita/LAMBDA-TYPES/LambdaDelta-1/C/defs/C_rect.con)
         .Π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
               →(Type:93192:cic:/matita/LAMBDA-TYPES/LambdaDelta-1/C/defs/C_rect.con)
         .λ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
               }