Top-level proofs for TypeClassLang

[hrutvik]

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.