Abstract | This report describes the elimination of the injectivity restriction for functional arithmetical interpretations as used in the systems $\mathcal{PF}$ and $\mathcal{PFM}$ in the Basic Logic of Proofs. An appropriate axiom system $\mathcal{PU}$ in a language with operators ``$x$ is a proof of $y$'' is defined and proved to be sound and complete with respect to all arithmetical interpretations based on functional proof predicates. Unification plays a major role in the formulation of the new axioms. |