Add/redefine (axiomatized) instances for redefined types

[sweirich]

If we redefine a type to axiomatize it:

redefine Axiom M.myType : Type.

It would be good to be able to add axiomatize a default instance for this type. Adding this instance in the midamble is too late --- a generated default instance or partial record selector may depend on it.

[antalsz]

How easy is this to work around?

[sweirich]

This isn't urgent. It turns out it is better to keep the type axiomatizations in a separate module instead of trying to add them to Core.v. That way we can break more module import cycles.