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 =
Show proof