DEFINITION bool_ind()
TYPE =
       ∀P:bool→Prop.(P true)→(P false)→∀b:bool.(P b)
BODY =
        assume P: bool→Prop
        suppose H: P true
        suppose H1: P false
        assume b: bool
          by cases on b we prove P b
             case true ⇒
                the thesis becomes the hypothesis H
             case false ⇒
                the thesis becomes the hypothesis H1
          we proved P b
       we proved ∀P:bool→Prop.(P true)→(P false)→∀b:bool.(P b)