DEFINITION True_ind()
TYPE =
       ∀P:Prop.P→True→P
BODY =
        assume P: Prop
        suppose H: P
        suppose H1: True
          by cases on H1 we prove P
             case I ⇒
                the thesis becomes the hypothesis H
          we proved P
       we proved ∀P:Prop.P→True→P