The concept of direct computation used by Statman (1977) was instrumental in the development of a notion of normal form for proofs of equality. On the other hand, the so-called Brouwer-Heyting-Kolmogorov interpretation of logical constants via the notion of proof-construction gave rise to a whole tradition of looking at proofs as terms in a functional calculus. Here we take a closer look at proof procedures for first-order sentences with equality drawing the attention to the need for introducing (function) symbols for rewrites. This leads us to a proposal to the effect that the framework of labelled natural deduction gives the right tools to formulate a proof theory for the “logical connective” of propositional equality in the style of the so-called Curry–Howard interpretation. The basic idea is that when analysing an equality sentence into (i) proof conditions (introduction) and (ii) immediate consequences (elimination), it becomes clear that one needs to bring in identifiers (i.e., function symbols) for sequences of rewrites, and this is what we claim is the missing entity in Per Martin-Löf’s equality types (both intensional and extensional). What we end up with is a formulation of what appears to be a middle ground solution to the ‘intensional’ vs. ‘extensional’ dichotomy which permeates most of the work on characterising propositional equality in natural deduction style.