Why 'let' can not be reduce to a lambda application in (extended) Calculus of Constructions
In an untyped language, those expressions would be equivalent. When working with types, instead, one might have a type while the other one has no type.

Assume that numbers and arithmetic operators all work on $\sf nat$. Then $e_0 = 2+2$ can be typed as $\sf nat$. Now, we can try to perform a $\beta$-expansion, i.e. to "apply $\beta$ backwards", and reach $e_1 = (\lambda x:{\sf nat}.\ x+2)2$.

$$(\lambda x:{\sf nat}.\ x+2)2 \to_\beta 2+2$$

This new expression $e_1$ would still have type $\sf nat$. But we could also go further
to $e_2=(\lambda \tau:{\sf Type}.\ (\lambda x:\tau.\ x+2)2){\sf nat}$.

$$(\lambda \tau:{\sf Type}.\ (\lambda x:\tau.\ x+2)2){\sf nat} \to_\beta(\lambda x:{\sf nat}.\ x+2)2 \to_\beta 2+2$$

Now, $e_2$ can not be typed. If it had a type, every subterm of $e_2$ would also be typeable, including $e_2' = (\lambda \tau:{\sf Type}.\ (\lambda x:\tau.\ x+2)2)$, but this subterm can not be typed. The only type we can assign here would be of the form

$$
e_2' : \prod_{\tau:{\sf Type}} (\mbox{something})
$$

in which case this would also be typeable:

$$
e_2' \, {\sf bool} \to_\beta (\lambda x:{\sf bool}.\ x+2)2
$$

The above is nonsense, since $2$ is not a $\sf bool$, so it should not be bound to $x$.

Indeed, we just discovered that types are not preserved under $\beta$-expansion.

A first question arises:


  Couldn't we $\beta$-reduce the expression before typing?


Yes, and that's (roughly) what ${\sf let}\ \tau = {\sf nat}\ {\sf in}\ e$ does: it types $e$ knowing that what $\tau$ actually is.

And now one might counter with:


  If $\sf let$ works in that way, why don't we use the same technique for lambdas?


We can't do that, since lambdas are not always immediately applied to an argument. The syntax ${\sf let}\ x = t\ {\sf in}\ e$ shows what is the value of $x$, namely $t$. The syntax $(\lambda x. e) t$ also shows the value of $x$ but not all lambdas are used in that way: sometimes we want to use $(\lambda x. e)$ without an argument. Say, we want to pass that to another function $F (\lambda x. e)$, or build a pair of functions $(\lambda x. e, \lambda x. e')$. Here, we don't know what $x$ is. Unlike the $\sf let$ case, here $x$ could even take many values, e.g. if $F = \lambda k. k 0 + k 1$ then $F (\lambda x. e)$ makes $x$ to be $0$ on one call and $1$ in the other call.

So, $\sf let$ is less general than a lambda, and we can have a "special" typing rule for that.