mathlib3

f8d8171d - refactor(logic/relator): turn *_unique and *_total into defs, not classes (#9135)

refactor(logic/relator): turn *_unique and *_total into defs, not classes (#9135) We had (almost) no instances for these classes and (almost) no lemmas taking these assumptions as TC arguments.