Prefix [Instance] with [Global]

[Instance]s are, by default, local to sections.  I've gone through and
prefixed all of the [Instance]s inside [Section]s of with [Global], so
they get picked up by typeclass search.  I don't think I missed any, but
I'm not sure.

This is especially useful for developments building on top of this
library which simply [Import HoTT] and want to prove contractibility
facts in an automated fashion.
Remove an [Existing Instance]

We don't need it, now that we declared that using [Global Instance]
rather than just [Instance] in a section.
Merge branch 'instances' of https://github.com/JasonGross/HoTT

Conflicts:
	theories/hit/minus1Trunc.v