So, this would be a definition of False in the Calculus of Constructions:
$$\bot = \forall x : \mathbf P . x$$
And, according to Wikipedia, this is an inference rule:
$${\Gamma \vdash A : K \qquad \Gamma , x : A \vdash B : L} \over {\Gamma \vdash (\forall x : A . B) : L}$$
Wouldn't this imply the following:
$$(\forall x : \bot . x) : \bot$$
Obviously this can't be the case, as this would provide a proof of $\bot$. Why is this proof incorrect though?
Additional context: I'm writing an automated proof checker and the above term proves False, which makes the program useless since it results in inconsistent logic.