DEFINITION K_ind()
TYPE =
       ∀P:K→Prop
         .(∀b:B.(P (Bind b)))→(∀f:F.(P (Flat f)))→∀k:K.(P k)
BODY =
Show proof