[ add ] lifting `{to|from}Witness` from `Relation.Nullary.Decidable.Core` to `Relation.Unary` and `Relation.Binary`

[jamesmckinna]

Specifically: for an IsDecEquivalence structure/DecSetoid bundle, it might be a useful enhancement to have proofs that the underlying relation
x ≈ y is equivalent to True (x ≟ y), and thus, for example, we have 'reflexivity modulo True' ie. x ≟ x ≡ yes _ etc. , cf. Relation.Binary.PropositionalEquality.{≡-≟-identity|≢-≟-identity} for analogues in the case for _≡_.

Issue: avoiding lots of repetitive reasoning by decision on x ≟ y, and going via contradiction in the non-equal case... etc.

Opportunity: potentially lots for downstream refactoring?

[JacquesCarette]

If it works, seems like a really good idea.

[jamesmckinna]

See #2737 , #2738 , and #2740 for some preliminary warm-ups for this in the important DecidableEquality case...

[jamesmckinna]

Probably worth trying to fold this in to #2952 , or as a separate v2.4 PR... this shouldn't be breaking?

[jamesmckinna]

But... it seems to further require in general that x ≈ y be Irrelevant (which it is in the DecidableEquality case, but probably nowhere else of interest?) so closing this as not really achievable. What had I been thinking?