Definitional proof irrelevance has proven to be a valuable feature to improve the ergonomics of proof assistants in a variety of mechanization scenarios, ranging from mathematics to certified programming. In particular, proof irrelevance is extremely useful for dealing with equality, allowing the proof assistant to automatically identify terms up to equality proofs. Lean was designed from the start with a proof irrelevant universe of propositions, while Rocq was recently extended with such a universe. Unfortunately, the metatheoretical status of equality in a proof irrelevant universe is challenging, with both canonicity and decidability issues reported in the literature. In this context, Lean and Rocq currently embody two unsatisfactory standpoints: in Rocq, proof-irrelevant equality can only be eliminated into other proof-irrelevant types, which ensures the good properties of the theory, but limits the applicability of this equality type for users; conversely, Lean unrestrictively embraces irrelevant equality with its full elimination principle, but without formal justification.

We consolidate the status of equality in a proof irrelevant universe by providing a complete formalized metatheoretic account of this combination. We start by observing that the computation rule for equality in Lean can be naturally strengthened to a more convenient one, and then prove both Lean’s original equality type and its strengthening satisfy expected properties. Concretely, we prove decidability of conversion, thus answering positively an open problem in the literature, and propositional canonicity, justifying an evaluation-via-erasure mechanism that allows reflecting external computations back into the theory. We implement these mechanisms as extensions to Rocq, to be integrated in its next release, and formalize all the metatheoretical results in Rocq. As such, this work informs the design and evolution of proof assistants that embrace definitional proof irrelevance, addressing key foundational open issues.