Introduce "type scheme entailment" to pick the best type scheme

[nikomatsakis]

The ty layer has a notion of "schemes" which are the result of proving something is true; they basically pair up a bunch of inference variables with relationships between those variables that must still be proven (e.g., ?T <= ?U).

Right now, the extract-schemes function takes multiple environments and yields potentially many schemes:

https://github.com/nikomatsakis/a-mir-formality/blob/9abc565ca76cb7bb613c18043b1bf092d0f0f844/src/ty/scheme.rkt#L13-L21

Often though some schemes are just better than others. We ought to be able to compute that by basically checking whether one scheme entails another. e.g. a scheme that says (?T <= ?U, ?T <= ?V) is just less good than (?T <= ?U) on its own, since the latter puts fewer constraints. We can compute this by seeing that the first scheme entails the other (i.e., it implies the other is true) but not vice versa. In that case, we prefer the entailed one.