Use _ind and _rec for eliminators, close #517

As proposed at #517, this uses `_ind` for the dependent eliminator and `_rec` for the nondependent one across the board.  There was a slight snag in implementing this for ordinary (non-higher) inductive types, because Coq's `induction` tactic appears to hardcode the suffixes `_rect`, `_rec`, and `_ind`.  So rather than making `_rect` a parsing notation for `_ind`, I made it a `Definition` for it, at least in the cases of inductive types defined by us.  In the case of inductive types defined in the coq stdlib file `Datatypes.v`, I left the definition of `_rect` there since (at least in some cases) it gets used by `induction` elsewhere in the stdlib, and then redefined the `_ind` version in our files.

Moreover, in the case of `nat` I had to leave Coq's version of `_rec` (meaning the dependent eliminator into `Set`) in `Datatypes.v`, since Coq's `nat` lands in `Set` and `induction` wants to use `_rec` when the target is in `Set`.  Then I created `Types/Nat.v` to hold a definition of `nat_ind` for us.  This raises another question, though: do we want to use the `nat` from the stdlib, and if so, should we modify the stdlib so that it doesn't land in `Set`?  Or should we define our own type `Nat` in `Types/Nat.v` the way we did for `Bool`?
Yeah... I'm not sure what we want.  It defaults to `Local`.  On the one hand, if it were `Global` then all other inductive definitions in the library would be forced to define their own elimination schemes, and thereby to conform to our naming conventions.  But on the other hand, people might be unpleasantly surprised (not to say confused) by defining an inductive type and then finding that `induction` and `elim` fail on it.  Maybe it should be `Local` and the style file should tell people that when they define an inductive type they should `Local Unset Elimination Schemes` first and then define the `_ind` and `_rec` schemes with `Scheme`?  That way people won't be taken by surprise, and if they don't conform to our naming conventions it can just be fixed later.