noticed something odd in our local simulation relation

theories/sim/local.v

@@ -58,7 +58,7 @@ Inductive _sim_local_body_step (r_f : A) (sim_local_body : SIM)
              (* For any new resource r' that supports the returned values are
                 related w.r.t. r' *)
              (VRET: vrel r' v_src v_tgt)
-             (WSAT: wsat (r_f ⋅ (rc ⋅ r')) σs' σt')
+             (WSAT: wsat (r_f ⋅ (rc ⋅ r')) σs' σt') (* FIXME this should not be needed, because [sim_local_body] already is of the shape [wsat → _] *)
              (STACK: σt.(scs) = σt'.(scs)),
         ∃ idx', sim_local_body (rc ⋅ r') idx'
                                (fill Ks (Val v_src)) σs'