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.

This approach sought to disallow infinite unfolding of the two type trees by not allowing *both* trees to simultaneously unfold recursive definitions more than once down matching structural paths (i.e. one side can unfold arbitrarily many times to match another's structure, but if both start unfolding down a particular path, we stop it after one unrolling) -- a sort of mutual contract/bound on their parallel search down the structures.  I thought it was a simple, elegant approach, but perhaps their are some obscure corner cases it doesn't cover? It works for all the current TR test suite. I'll have to go look into those other approaches (the subtype/infer approaches) more. Question: is subtype* from 'subtype.rkt' an example of the other approach? That function is > 400 LOC! =)