# in type theory does (x:A) imply ((x:A):A)

In the formulation of type theory I'm reading, (x:A) is an expression of type A. This would seem to imply ((x:A):A) and (((x:A):A):A)... Is this a common feature of type theories? Or am I reading too much into an ambiguous sentence?

-
$$(\lambda x.\ x) : (\alpha \to \mathtt{int})$$ (note that here the most general type for $\lambda x.\ x$ is $\alpha \to \alpha$) which would result in a value of type $\mathtt{int} \to \mathtt{int}$.