Data.Vec.Equality: add more conversions

These are all in PropositionalEquality (even the ones proving
heterogeneous equalities) because the implementations depend on each
other. To make this right, I'd either mutually recursive modules (is
this possible) or have three separate modules: one with to-≡ and from-≡,
one with to-≅, and one with to-subst-≡. The order I used for these
modules is the dependency order of the implementations.
Data.Vec.Equality: add more generic equality converter

This reduces more general code, but I think the return type is less
useful.

WDYT? Should this be dropped?