DEFINITION nat_rec()
TYPE =
       ΠP:nat→Set
         .(P O)→(Πn:nat.(P n)→(P (S n)))→Πn:nat.(P n)
BODY =
Show proof