DEFINITION B_ind()
TYPE =
       ∀P:B→Prop
         .(P Abbr)→(P Abst)→(P Void)→∀b:B.(P b)
BODY =
        assume P: B→Prop
        suppose H: P Abbr
        suppose H1: P Abst
        suppose H2: P Void
        assume b: B
          by cases on b we prove P b
             case Abbr ⇒
                the thesis becomes the hypothesis H
             case Abst ⇒
                the thesis becomes the hypothesis H1
             case Void ⇒
                the thesis becomes the hypothesis H2
          we proved P b
       we proved 
          ∀P:B→Prop
            .(P Abbr)→(P Abst)→(P Void)→∀b:B.(P b)