Commit 2020-08-15 19:14 8ce00af6
View on Github →feat(data/set/basic): pairwise_on for equality (#3802)
Add another lemma about pairwise_on: if and only if f takes
pairwise equal values on s, there is some value it takes everywhere
on s. This arose from discussion in #3693.