As brought up in #92, the theorems in IndexedSet.lagda.md should be extracted to their own module in src/Vatras/Data/IndexedSet/Properties.agda to follow the conventions from the standard library. Currently, IndexedSet.lagda.md contains all definitions and theorems.
As brought up in #92, the theorems in
IndexedSet.lagda.mdshould be extracted to their own module insrc/Vatras/Data/IndexedSet/Properties.agdato follow the conventions from the standard library. Currently,IndexedSet.lagda.mdcontains all definitions and theorems.