DEFINITION nat_rec()
TYPE =
       ΠP:nat→Set
         .(P O)→(Πn:nat.(P n)→(P (S n)))→Πn:nat.(P n)
BODY =
λP:nat→Set
         .λp:P O
           .λf:Πn:nat.(P n)→(P (S n))
             .FIXaux{aux:Πn:nat.(P n):=λn:nat.<P> CASE n OF O⇒p | S n1⇒f n1 (aux n1)}