In the wikipedia article on the Lambda cube, does the Application rule apply to all terms or just to variables?

Question

The Application inference rule in the wikipedia page on the Lambda cube is given as $$\frac{\Gamma \vdash C\colon \Pi x\colon A. B\quad \Gamma \vdash a\colon A}{\Gamma \vdash Ca\colon B[a/x]}.$$

Is $a$ exclusively a variable, or could $a$ be a term? That is, would it be correct to replace $a$ by $D$?

Answer 1

$a$ stands for a term. It's a metavariable, if you like, while $x$ is a variable.