Add w4_unint_rme proof script

[glguy]

While SAW already has an rme proof script this version uses the version behind What4 allowing it to take advantage of the preexisting uninterpreted function support.

I've been testing this out as a part of my Ascon verification exercise

[RyanGlScott]

Please add a test case. Otherwise, LGTM.

[sauclovian-g]

Are you going to release the RME changes on Hackage before / as part of the impending overall release? If so, do we want this change in the SAW release? @aschwerdfeger-galois fyi

[RyanGlScott]

I don't know if we care too much about getting this into the next SAW release or not, as we are mostly using nightly SAW in our developments. That being said, making a Hackage release of rme is fairly cheap, and it would be worth doing anyway, I'd say.