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 =
λP:K
               →(Type:91128:cic:/matita/LAMBDA-TYPES/LambdaDelta-1/T/defs/K_rect.con)
         .λf:Πb:B.(P (Bind b))
           .λf1:Πf1:F.(P (Flat f1)).λk:K.<P> CASE k OF Bind b⇒f b | Flat f2⇒f1 f2