Tidy up a type checker Note
Note [Checking telescopes] in
Note [Keeping scoped variables in order: Explicit] seem to be covering much the same ground. The former is more detailed. Is there any reason to keep the original one around? Even if there is, we should de-duplicate these notes; I can't tell the difference in what they try to address.