rewrite each: make sure to normalize/unfold each side

src/checker/Pulse.Checker.AssertWithBinders.fst

@@ -269,6 +269,13 @@ let rewrite_all (is_source:bool) (g:env) (p: list (term & term)) (t:term) : T.Ta
           (fst (Pulse.Checker.Pure.instantiate_term_implicits g e2 None false)))
         p
     in
+    let p : list (R.term & R.term) =
+      T.map
+        (fun (e1, e2) ->
+          dfst <| Pulse.Checker.Prover.normalize_slprop g e1,
+          dfst <| Pulse.Checker.Prover.normalize_slprop g e2)
+        p
+    in
     let lhs, rhs = visit_and_rewrite_conjuncts_all is_source g p t in
     debug_log g (fun _ -> Printf.sprintf "Rewrote %s to %s" (P.term_to_string lhs) (P.term_to_string rhs));
     lhs, rhs

test/nolib/RewriteEachUnfold.fst

@@ -0,0 +1,16 @@
+module RewriteEachUnfold
+
+#lang-pulse
+open Pulse.Nolib
+
+assume val foo : slprop
+assume val baz : slprop
+unfold let bar = foo
+
+fn test (_ : squash (foo == baz))
+  requires bar
+  ensures  baz
+{
+  rewrite each bar as baz;
+  ()
+}