Add heterogenous equality to Mr. Solver for SHA512 example

[m-yac]

This PR gets round_16_80 |= round_16_80_spec from the SHA512 example working by primarily adding heterogeneous equality to Mr. Solver. It also makes a few other changes, but instead of listing them here, I broke each change into its own commit. Each commit should be self-explanatory.

I'm not totally sure about the interface choices I made in SMT.hs in 45de464 (e.g. mrProveEq vs. mrProveRel, using a Bool to indicate heterogeneous equality), so that's definitely worth taking a look at. It's worth saying that I went for mrProveRel instead of something like mrProveHetEq because we will likely eventually want to add a parameter to this function which additionally lets the user give a custom relation for function terms (for lifetimes).

[eddywestbrook]

Looks good!