[enricozb]

Proof irrelevance I don't think is accepted in constructivist situations. Those are, however, not that relevant to the recent wave of AI math which uses Lean, whose type system includes classical mathematics.