DEFINITION True_ind()
TYPE =
       ∀P:Prop.P→True→P
BODY =
Show proof