DEFINITION K_rec()
TYPE =
       ΠP:K→Set
         .Πb:B.(P (Bind b))
           →(Πf:F.(P (Flat f)))→Πk:K.(P k)
BODY =
λP:K→Set
         .λ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