Anton Trunov

This is also very helpful for subset types. You don't need axioms to work with subset types if you have decidable equality.

@murbard No objections as well, feel free to release.

"Retry" sounds good! Or if I redefine the variable (like the variable `E` of problem 28) I'd like to have my solution re-checked. E.g. right now it seems that redefining...

I forgot to mention it, but the name `unit_irrelevance` is a bit confusing, as e.g. `eqtype.bool_irrelevance` is proof irrelevance for booleans: ```coq Lemma bool_irrelevance (x y : bool) (E E'...

@CohenCyril I opened a new issue for your last comment -- math-comp/math-comp#229

I'm almost sure there is (or at least was) a theorem like `unit_irrelevance` in our library (FCSL), so I think it would make sense to move it to math-comp. What...

> I am curious though about the use it may have in FCSL and whether it could be replaced by unitE. I tried to find it but could not, it...

A workaround here would be to just have the changes in the markdown files. I'll regenerate the rest of the files in a separate PR

Looks like something went wrong with the rebase:

Great! Any pointers/suggestions you might have regarding UI/UX or implementation of this feature?