Add utilities to use unsafe equality proofs

It's generally best practice to limit unsafe equalities as much as
possible, to avoid mistakes. A good way to do that is to use
`unsafeEqualityProof` to produce fake evidence of the smallest equality
needed. For example, if you know that `A` and `P` are sufficiently
similar and you need to coerce `[A] -> B -> C` to `[P] -> B -> C`, it's
much nicer to explicitly introduce fake evidence that `A ~ P` than to
use `unsafeCoerce` and hope you aren't accidentally coercing some
unrelated things elsewhere in the type.

Unfortunately, actually using the limited fake evidence can be tricky.
You might think you could write something like

```haskell
cabc :: ([A] -> B -> C) -> [P] -> B -> C
cabc f = case unsafeEqualityProof @A @P of
  UnsafeRefl -> f
```

But this won't work! When type checking the case branch, GHC rejects
`A ~ P` without even noticing that there's evidence for it available. This
means that more explicit utilities are needed to manipulate unsafe
equalities. One simple option would be to offer just a single function

```haskell
unsafeEqualityProofToEquality :: UnsafeEquality a b -> a :~: b
unsafeEqualityProofToEquality UnsafeRefl = Refl
```

Then people could use the utilities in `Data.Type.Equality` to manipulate
the resulting equality. But it seems to me that it's much nicer to
help users keep equality proofs *obviously* unsafe right up to the
point of use, to avoid a sort of "equality blindness". This commit
adds versions of the various equality proof functions in
`Data.Type.Equality` for `UnsafeEquality`, along with a few more
for convenience inspired by the Agda standard library.