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