Use explicit substitutions and WHNFs in the type checker

[brendanzab]

Currently we do eager substitutions under binders. This is inefficient and probably won't be tenable once we have recursive datatypes and definitions. Type systems like F* and PiSigma use weak head normal forms and explicit substitutions to get around this.

See also: https://github.com/brendanzab/pikelet/issues/22#issuecomment-381979497

[brendanzab]

One interesting thing that PiSigma does is reuse let bindings for explicit substitutions. This couild help us simplify the internals. Let bindings also use contexts internally, so this could further simplify our calculus.