Commit 2023-11-20 01:56 8b144faa
View on Github →refactor(Logic/Unique): remove dependency on Fin (#8510)
Unique should be available earlier than results about Fin n, by virtue of being a very basic logic typeclass with no dependencies on Nat or algebra.
This also generalizes some of the moved instances and lemmas.
There are no new declarations in this PR, only renames of existing ones.