@gallais @ltchen Rocq's Prop is proof irrelevant! At least for some people. The terminology differs. Some people are saying proof irrelevant for "proofs can't matter" or "proofs are erasable for computation". In this usage, the irrelevance you probably have in mind is called "uniqueness of proofs". I learned this from @andrejbauer