Until is a notoriously difficult temporal operator as it is both existential and universal at the same time: $A \cup B$ holds at the current time instant $w$ iff either $B$ holds at $w$ or there exists a time instant $w'$ in the future at which $B$ holds and such that $A$ holds in all the time instants between the current one and $w'$. This "ambivalent" nature poses a significant challenge when attempting to give deduction rules for until. In this paper, in contrast, we make explicit this duality of until by introducing a new temporal operator that allows us to formalize the “history” of until, i.e., the “internal” universal quantification over the time instants between the current one and $w'$. This approach provides the basis for formalizing deduction systems for temporal logics endowed with the until operator. For concreteness, we give here a labeled natural deduction system for a linear-time logic endowed with the new history operator and show that, via a proper translation, such a system is also sound and complete with respect to the linear temporal logic LTL with until. Reporting on joint work with Andrea Masini and Marco Volpe.