DEFINITION K_rect()
TYPE =
       ΠP:K
                →(Type:91128:cic:/matita/LAMBDA-TYPES/LambdaDelta-1/T/defs/K_rect.con)
         .Πb:B.(P (Bind b))
           →(Πf:F.(P (Flat f)))→Πk:K.(P k)
BODY =
Show proof