# 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?

-
My guess would be that $(x:A)$ is only assumed to be an expression of type $A$ when $x$ is a variable. Therefore, since $(x:A)$ is not a variable, probably $((x:A):A)$ is not well-formed. –  goblin Jun 17 '14 at 19:20

$$(\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}$.