Unify the location of passing arguments to Coq

This way, when we change them in the next commit or the future, we only
have to do it in one place.
Strip out the standard library replacement

Instead replace the relevant constants on top of the standard library.
This is less nice, because it allows access to the evil [eq], but it
means we can use lemmas in the standard library about things like [le]
and [nat] and [bool].  Also tactics.  Also, we won't have to port and
maintain the whole standard library.  Also (the real reason here) I
couldn't figure out how to get the replacement to compile with Coq
trunk, and I want to ease the (eventual) switch to trunk.

We should be able to strip out the constants from the standard library
replacement file, as they become polymorphic in trunk.  (I'm still
holding out hope that the standard library [sigT] of 8.5 will be both
polymorphic and a primitive record.