DEFINITION nat_rect()
TYPE =
       ΠP:nat
                →(Type:2793:cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/nat_rect.con)
         .(P O)→(Πn:nat.(P n)→(P (S n)))→Πn:nat.(P n)
BODY =
λP:nat
               →(Type:2793:cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/nat_rect.con)
         .λ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)}