We define an alternative representation for types in the simply typed $\lambda$-calculus or equivalently for formulas in the implicational fragment of intuitionist propositional logic, which gives us a better insight on the nature of a types structure and its relation to the structure of the set of its normal inhabitants. Based on this representation of a type $\varphi$, called its formula-tree, we define the notion of a valid proof-tree. Any such valid proof-tree represents a finite set of normal inhabitants of $\varphi$ and every normal inhabitant corresponds to exactly one valid proof-tree, constructable with the primitive parts in the formula-tree of $\varphi$. Precise algorithms are given to establish this relation. This method can be used to easily recognize and prove results concerning inhabitation/provability.