Perfect, that's what I was thinking; thank you for clarifying.

Second, on your second bolded point...My audience generally uses typed languages like this: first specify what the vocabulary is, along with each bit of vocabulary's grammatical category; then use that vocabulary to formulate grammatical expressions of type t which comprise a formal theory of something. It sounds like you're saying that the way this would go, in comp sci, is more `all at once': specify both the vocabulary and associated grammatical categories in a way which (implies terms of type t which?) comprises a formal theory of that same something. Is that right?

Thank you, this is very helpful. Two follow-ups. First: the problem which motivated my first question seems to arise even if Consistency is denied. Variables also implies that there is a variable $\nu$ such that $\nu\mathbin{:}(\Pi x\mathbin{:}\ast.\ast)$ is an expression; so $(\Pi x\mathbin{:}\ast.\ast)$ is inhabited; and so once again, the standard definition of consistency is violated. Do I have that right?