definition pred: nat \to nat \def
\lambda n:nat. match n with
[ O \Rightarrow O
| (S p) \Rightarrow p ].
theorem pred_Sn : \forall n:nat.n=(pred (S n)).
definition pred: nat \to nat \def
\lambda n:nat. match n with
[ O \Rightarrow O
| (S p) \Rightarrow p ].
theorem pred_Sn : \forall n:nat.n=(pred (S n)).