The rule of \(\N\)-elimination simultaneously expresses the type of a function defined by primitive recursion and, under the Curry-Howard interpretation, the rule of mathematical induction: we prove the property \(C\) of a natural number \(x\) by induction on \(x\).