Commit 2023-11-20 01:56 8b144faaView on Github →
refactor(Logic/Unique): remove dependency on
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.