# Commit 2022-06-10 07:36 5bccb515

View on Github →refactor(logic/equiv/basic): tweak lemmas on equivalences between `unique`

types (#14605)
This PR does various simple and highly related things:

- Rename
`equiv_of_unique_of_unique`

to`equiv_of_unique`

and make its arguments explicit, in order to match the lemma`equiv_of_empty`

added in #14604. - Rename
`equiv_punit_of_unique`

to`equiv_punit`

and make its argument explicit to match`equiv_pempty`

. - Fix their docstrings (which talked about a
`subsingleton`

type instead of a`unique`

one). - Move them much earlier in the file, together with the lemmas on empty types.
- Golf
`prop_equiv_punit`

.