Implement "TypeLevelReasoning" proposal at wiki:TypeLevelReasoning

This commit includes a propositional equality (:=:) in Data.Type.Equality,
a Proxy type in Data.Proxy, and has updates to Typeable.

There is an unfortunate number of hs-boot files necessary, but that
seems cleaner than moving Typeable instances around willy-nilly.