Question on the "Tutorial implementation of dependently typed lambda calculus"
$\mathsf{id}$ and $\mathsf{const}$ are not variables of the calculus, but syntactic sugar for $\lambda x \rightarrow x$ and $\lambda x \rightarrow \lambda y \rightarrow x$ respectively. This is stated at the end of §2.2 and subtly conveyed by the use of a sans-serif font rather than italics (this is a typographic convention of this particular document, not a common convention).
So for example the type judgement
$$
\alpha :: \ast, y :: \alpha \vdash (\mathsf{id} :: \alpha \rightarrow \alpha) \: y :: \rightarrow \alpha
$$
is also the type judgement
$$
\alpha :: \ast, y :: \alpha \vdash (\lambda x \rightarrow x :: \alpha \rightarrow \alpha) \: y :: \rightarrow \alpha
.
$$
It's a different notation for the same mathematical object.