Commit 2022-06-10 07:36 5bccb515

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.