Add "From HoTT" before many "Require" commands

[jdchristensen]

I added "From HoTT " before Require lines that listed Basics, but not if they listed HoTT.Basics or Basics.Overture, for example. So this is as small as change as possible.

Closes #2290

[jdchristensen]

Unfortunately, we can't add From HoTT everywhere. For example, in FreeGroup.v, we have Require Import ... Group ..., and From HoTT Require Import Group fails because of the file Group.v in the test/ folder, which is mapped to HoTT.Tests. For now, I just avoided this, but in the long run having the test/* files and the theories/* files conflict in the HoTT namespace is not a good idea. cc: @Alizter

[jdchristensen]

Ok, this builds and is ready for review.

[jdchristensen]

I'll go ahead and merge, but if anyone has thoughts for improvements, I'm happy to make them later.