I would suggest just adding proof irrelevance as an axiom to the theory. This also makes subtypes more convenient. I.e., if one has a set S and a property P: S

I would suggest just adding proof irrelevance as an axiom to the theory. This also makes subtypes more convenient. I.e., if one has a set S and a property P: S -> Prop, the subset of S where the property is satisfied, in coq notation, { s: S, P s }, has with proof irrelevance automatically as many elements as there are elements in S that satisfy P. Without proof irrelevance one often finds oneself proving proof irrelevance for specific propositions that are needed for subtypes or even changing the definition of P such that proof irrelevance becomes provable.