Implicit pairwise arguments

Stream: general

[Yaël Dillies]

I'm changing docs#set.pairwise from ∀ x ∈ s, ∀ y ∈ s, x ≠ y → r x y to ∀ ⦃x⦄, x ∈ s → ∀ ⦃y⦄, y ∈ s → x ≠ y → r x y. Should I do the same to docs#pairwise?

[Mario Carneiro]

There is no analogue of that change for docs#pairwise, since there are no membership assumptions in that case

[Yaël Dillies]

I don't know what you want to call it, if not "analog", but here's the change I want to make:

• Currently: ∀ i j, i ≠ j → r i j
• What I want: ∀ ⦃i j⦄, i ≠ j → r i j

[Eric Wieser]

I'd caution against changing both in the same PR