DEFINITION nat_ind()
TYPE =
       ∀P:nat→Prop
         .(P O)→(∀n:nat.(P n)→(P (S n)))→∀n:nat.(P n)
BODY =
Show proof