Why does Coq include let-expressions in its core language

Question

Coq includes let-expressions in its core language. We can translate let-expressions to applications like this: let x : t = v in b ~> (\(x:t). b) v I understand that this does not always work because the value v would not be available when typechecking b. However this can be easily fixed by special casing the typechecking of applications of the form (\(x:t). b) v. This allows us to remove let-expressions at the cost of a special case while typechecking. Why does Coq include still include let-expressions? Do they have other advantages (besides not needing the special case)?