preventing automatic type inference have been fixed.
match n with
[ O \Rightarrow O
| (S p) \Rightarrow
match n with
[ O \Rightarrow O
| (S p) \Rightarrow
- [\lambda n:nat.nat] match m with
[O \Rightarrow (S p)
| (S q) \Rightarrow minus p q ]].
[O \Rightarrow (S p)
| (S q) \Rightarrow minus p q ]].
match n with
[ O \Rightarrow true
| (S p) \Rightarrow
match n with
[ O \Rightarrow true
| (S p) \Rightarrow
- [\lambda n:nat.bool] match m with
[ O \Rightarrow false
| (S q) \Rightarrow leb p q]].
[ O \Rightarrow false
| (S q) \Rightarrow leb p q]].