let-aliasing + removing let imps

First draft of proposal to remove implications from the let typing judgment (replaced by a logically equivalent or) and add aliasing for let-bindings where the expression being bound has an object (e.g. x, (car y), etc...).

This speeds up type checking (e.g. the 'filters-more' function from http://bugs.racket-lang.org/query/?cmd=view&pr=14838) and adds the ability to typecheck expressions that utilize simple let bindings of pure expressions, such as the following function:

#lang typed/racket

(: foo (Any -> Number))
(define (foo x)
  (match x
    [(? number?) x]))


The current implementation has 2 errors when running the unit tests at the moment, which relate to usages of types with '...' such as:

(let: ((f : (All (b ...) (Any ... b -> Any)) (lambda x (quote x)))) (lambda xs (apply f (quote y) xs)))

Obviously I need to work out these errors before this is pulled, but this is what it looks like at the moment, FYI.

Yes, `subtype*` is an example of the other approach. But it's nicely explained in the chapter of Pierce on subtyping equi-recursive types.

I think your approach breaks with mutual recursion (because we can only remember one thing at a time.