Rewrite should prove resource before checking equal;ity

[mtzguido]

#lang-pulse
open Pulse

assume val foo : slprop
assume val bar : slprop

fn test ()
  requires emp
  ensures emp
{
  rewrite foo as bar;
}

This gives:

- rewrite: could not prove equality of
- foo
- bar
- Assertion failed
- The SMT solver could not prove the query. Use --query_stats for more details.

But it would be nicer if instead we got the error that foo cannot be proven before this, and highlighting only foo.