Commit 2024-04-18 05:39 c92f1eed

View on Github →

feat: make ExistsUnique notation throw an error when used with more than one binder (#12218) Zulip discussion

Estimated changes

modified theorem Setoid.classes_eqv_classes
modified theorem Setoid.eq_eqv_class_of_mem
modified theorem Setoid.eq_of_mem_eqv_class
modified theorem Setoid.eqv_class_mem'
modified theorem Setoid.eqv_class_mem
modified theorem Setoid.eqv_classes_disjoint
modified def Setoid.mkClasses