DEFINITION K_ind()
TYPE =
       ∀P:K→Prop
         .(∀b:B.(P (Bind b)))→(∀f:F.(P (Flat f)))→∀k:K.(P k)
BODY =
        assume P: K→Prop
        suppose H: ∀b:B.(P (Bind b))
        suppose H1: ∀f:F.(P (Flat f))
        assume k: K
          by cases on k we prove P k
             case Bind b:B ⇒
                the thesis becomes P (Bind b)
                by (H .)
P (Bind b)
             case Flat f:F ⇒
                the thesis becomes P (Flat f)
                by (H1 .)
P (Flat f)
          we proved P k
       we proved 
          ∀P:K→Prop
            .(∀b:B.(P (Bind b)))→(∀f:F.(P (Flat f)))→∀k:K.(P k)