[ 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 ≈ z is equivalent to True (x ≟ y), and thus, for example, we have 'reflexivity modulo True' ie. x ≟ x ≡ true etc.

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.