DEFINITION bool_ind()
TYPE =
       ∀P:bool→Prop.(P true)→(P false)→∀b:bool.(P b)
BODY =
Show proof