Global instances

This is an alternative to #134 which ensures that we haven't missed any newly declared `Instance`s.  I'm not sure about the `Existing Instances` in `theories/hit/epi.v`, so I left them alone; is there a reason that we don't declare those `Theorem`s as `Instance`s where we prove them?