> The type theories of Lean and Rocq are fairly close, with the exception that Lean operates with definitional proof irrelevance as one of the default axioms. This causes Lean to lose subject reduction and decidability of definitinal equality as properties of the language.

Couldn't you introduce proof relevance as an explicit axiom into a Lean program to solve that particular issue?