Add `-cong` aliases to proofs in `Data.X.Relation.Binary.Equality`

[mechvel]

In lib-1.1, Data.List.Relation.Binary.Equality.Setoid shows several lemmas like

++⁺ : ∀ {ws xs ys zs} → ws ≋ xs → ys ≋ zs → ws ++ ys ≋ xs ++ zs
...
concat⁺ : ∀ {xss yss} → Pointwise _≋_ xss yss → concat xss ≋ concat yss

But they are all of congruence, so that they need to be called ++-cong-≋ , concat-cong-≋≋ and so on. For example, *-cong of Semiring is not called *⁺. ?

[MatthewDaggitt]

The names come from a naming scheme that generalises to all relations, rather than just equality (see the style guide).

If you want, feel free to open a PR adding in the congruence aliases as well. I'd leave the -≋ out of the names though, as it's implicit from the module they are exported from.