Why does Coq include let-expressions in its core language
It is a common misconception that we can translate let-expresions to applications. The difference between let x : t := b in v and (fun x : t =&gt; v) b is that in the let-expression, during type-checking of v we know that x is equal to b, but in the application we do not (the subexpression fun x : t =&gt; v has to make sense on its own).

Here is an example:

(* Dependent type of vectors. *)
Inductive Vector {A : Type} : nat -&gt; Type :=
  | nil : Vector 0
  | cons : forall n, A -&gt; Vector n -&gt; Vector (S n).

(* This works. *)
Check (let n := 0 in cons n 42 nil).

(* This fails. *)
Check ((fun (n : nat) =&gt; cons n 42 nil) 0).


Your suggestion to make application (fun x : t =&gt; v) b a special case does not really work. Let us think about it more carefully.

For example, how would you deal with this, continuing the above example?

Definition a := (fun (n : nat) =&gt; cons n 42 nil).
Check a 0.


Presumably this will not work because a cannot be typed, but if we unfold its definition, we get a well-typed expression. Do you think the users will love us, or hate us for our design decision?

You need to think carefully what it means to have the "special case". If I have an application e₁ e₂, should I normalize e₁ before I decide whether it is a $\lambda$-abstraction? If yes, this means I will be normalizing ill-typed expressions, and those might cycle. If no, the usability of your proposal seems questionable.

You would also break the fundamental theorem which says that every sub-expression of a well-typed expression is well-typed. That's as sensible as introducing null into Java.