Girard-Reynolds polymorphic lambda calculus [Girard71,Reynolds74], also known as system $\mathbf{F}$, is an elegant system introduced in the early seventies with only two generators of types (formulas): implication and second-order universal quantification. Its impredicative feature - second-order quantifications may instantiate arbitrary types - explains the remarkable expressive power of $\mathbf{F}$ but also the difficulty of reasoning about the system. In the present talk we are interested in a predicative variant of system $\mathbf{F}$, known as the atomic polymorphic calculus [Ferreira06], or system $\mathbf{F}_{\mathbf{at}}$. $\mathbf{F}_{\mathbf{at}}$ has the exact same types (formulas) as $\mathbf{F}$, but a severe restriction on the range of the type variables: only atomic universal instantiations are allowed. We present $\mathbf{F}_{\mathbf{at}}$ and give an overview of some proof-theoretic properties of the system such as the strong normalization property [FerreiraFerreira12], the subformula property [Ferreira06], the sound and faithful embedding of the full intuitionistic propositional calculus into $\mathbf{F}_{\mathbf{at}}$ [FerreiraFerreira09, FerreiraFerreira2015], the disjunction property [Ferreira06], etc. Moreover, we claim that $\mathbf{F}_{\mathbf{at}}$ is the proper setting for the intuitionistic propositional calculus, avoiding this way the connectives $\bot$ and $\vee$, whose natural deduction elimination rules have been subject to harsh criticism (see [Girard(1989B)] pages 74, 80), and avoiding the ad hoc commuting conversion needed in the usual presentation of the latter calculus.