Top-level proofs for TypeClassLang

The top-level result for TypeClassLang should state:
- given a well-annotated TypeClassLang program
- there should be a valid translation to a PureLang program
- which is itself well-typed (and therefore safe)

Though prior work has considered Core-like/System-F like languages with higher-rank polymorphism, we should hopefully be able to show type preservation for simple types - but this remains to be seen.

Review the existing TypeClassLang and PureLang definitions, along with the prior work on Core-like or System-F-like languages mentioned in the issue. Determine the formal statement and proof obligations for translating well-annotated TypeClassLang programs into well-typed PureLang programs; done means the top-level type-preservation and safety result is established.

Written by the indexing model from the issue text.