[ 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...