equiv between subsingletons

Stream: general

[Johan Commelin]

I want to prove an equiv between two subsingletons. Is there a little lemma in mathlib that says I don't have to check that the compositions are the identity?

[Kenny Lau]

subsingleton.elim?

[Johan Commelin]

That doesn't do exactly what I want, right? I could use it, but it would lead to an obfuscated proof of something that is math-trivial anyway.