DEFINITION nat_ind()
TYPE =
       ∀P:nat→Prop
         .(P O)→(∀n:nat.(P n)→(P (S n)))→∀n:nat.(P n)
BODY =
        assume P: nat→Prop
        suppose H: P O
        suppose H1: ∀n:nat.(P n)→(P (S n))
          (aux) by well-founded reasoning we prove ∀n:nat.(P n)
          assume n: nat
             by cases on n we prove P n
                case O ⇒
                   the thesis becomes the hypothesis H
                case S n1:nat ⇒
                   the thesis becomes P (S n1)
                   by (aux .)
                   we proved P n1
                   by (H1 . previous)
P (S n1)
             we proved P n
∀n:nat.(P n)
          done
          consider aux
          we proved ∀n:nat.(P n)
       we proved 
          ∀P:nat→Prop
            .(P O)→(∀n:nat.(P n)→(P (S n)))→∀n:nat.(P n)