bUnion/bInter/bsupr/binfi lemmas

Stream: general

[Yury G. Kudryashov]

Is there any reason to (a) use x ∈ s instead of (x) (hx : p x) in bUnion etc? (b) assume that the inner expression does not depend on hx?

[Mario Carneiro]

If you generalize them enough it will become "Union, twice"