DEFINITION K_rec()
TYPE =
       ΠP:K→Set
         .Πb:B.(P (Bind b))
           →(Πf:F.(P (Flat f)))→Πk:K.(P k)
BODY =
Show proof