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)