fixes #1248 (`to_set` / `xsection`)

[affeldt-aist]

Motivation for this change

TODO: maybe also rename xsection to xsect, that's clear enough.

Checklist

• [ ] added corresponding entries in CHANGELOG_UNRELEASED.md

• [ ] added corresponding documentation in the headers

Reference: How to document

Reminder to reviewers

• Read this Checklist
• Put a milestone if possible
• Check labels

[affeldt-aist]

@zstone1 what do you think about replacing the local notations to_set? surely that does not make proofs shorter, I was hoping to be able to reuse lemmas about xsection but it is not obvious they help

[affeldt-aist]

I think that there are more advantages than disadvantages so I undrafted this PR:

• to_set and xsection are essentially duplicates (one is Prop, the other is bool) so getting rid of one of them is good
• xsection is more "robust" because it is a definition and is better instrumented with lemmas, to_set was a repeated local notation that did not parse well

I think that this offsets the more verbose proofs.

[zstone1]

I agree, the way to_set worked was unsatisfactory. This at least consolidates the definition into one place, rather that redefining it. I'm happier with this (and I wouldn't use xsect, this notation isn't widely used enough for me to worry about saving the 3 characters)