Universal/existential quantification?
It helps to remember that $\forall$ (or $\Pi$ as you sometimes see) is a type. It's generalizing $\to$. So while it makes perfect sense to say $(\lambda x : A. M)\ N$, it doesn't make sense to say $(\forall x : A. M)\ N$ because $\forall ...$ is just a type. You wouldn't say $(A \to B)\ N$ becaues $\to$ isn't for computing per-se, it's there to classify lambda terms which can be applied like this.

This was something that tripped me up as well, but this is how the calculus of constructions (as well as any other dependently typed system is defined).

The two programs you wrote have very different intentions and the first one is ill-typed. It doesn't make sense to say $\forall x : A.\ \lambda x.\ x$ because $\forall$ requires both its arguments by types which means that if $\forall x : A. B$ is to be well-typed, we must have $B : *$. However, $\lambda x. x$ isn't a type, it can only ever be assigned a type of the form $\forall x : A. B$, never $*$. The second one on the other hand is almost (I think you meant to return $a$ not $x$) is a function and is given a type using two $\forall$s.