Too sleepy to go on. Committing what I have now.
Merge branch 'master' into brazil-universal-hints
First version of universal hint matching
Some progress on advice checking
Clarify universe indices, re-introduce G

Even if G can be derived using EQ-REFLECTION, we should still have it
because HTS does.
Strong normalization

The declarative part now needs some equations which commute coerce and
type names, e.g., when can we exchange `coerce` and `pi`?
Strong normalization
Normalize universal hints
Universal hints starting to work
Generalized hints compile. I bet they don't work.
Why doesnt github app delete files?
Fixing universal hints, working better now.
Merge branch 'brazil-universal-hints'