[ refactor ] `Data.Fin.Properties` of decidable equality, plus knock-ons#2740

MatthewDaggitt merged 28 commits intoagda:masteragda/agda-stdlib:masterfrom

jamesmckinna:refactor-Fin-propertiesjamesmckinna/agda-stdlib:refactor-Fin-propertiesCopy head branch name to clipboard