diff --git a/src/ecPV.ml b/src/ecPV.ml
index 3d173b9b6..d25f946a3 100644
--- a/src/ecPV.ml
+++ b/src/ecPV.ml
@@ -1127,6 +1127,11 @@ module Mpv2 = struct
       when EcReduction.EqTest.for_type env ty1 ty2
         && EcReduction.EqTest.for_type env b1.e_ty b2.e_ty ->
       List.fold_left2 (add_eqs_loc env local) eqs (b1::es1) (b2::es2)
+    | _, _ when EcReduction.EqTest.for_expr env e1 e2 -> 
+      let fv1 = e_read env e1 in
+      let fv2 = e_read env e2 in
+      union eqs (eq_refl (PV.union fv1 fv2))
+
     | _, _ -> raise EqObsInError
 
   let add_eqs env e1 e2 eqs =  add_eqs_loc env Mid.empty eqs e1 e2
diff --git a/src/ecReduction.ml b/src/ecReduction.ml
index d28cb2058..e268dab4e 100644
--- a/src/ecReduction.ml
+++ b/src/ecReduction.ml
@@ -185,7 +185,7 @@ module EqMod_base(Fe : sig
   val for_expr : env -> norm:bool -> (ident * ty) Mid.t -> expr -> expr -> bool
 end) = struct
   open EqTest_base
-  open Fe
+  include Fe
 
   (* ------------------------------------------------------------------ *)
   let rec for_stmt env alpha ~norm s1 s2 =
@@ -1866,8 +1866,9 @@ module EqTest = struct
 
   include EqMod_base(struct
     let for_expr env ~norm:_ alpha e1 e2 =
+      let dummy_mem = EcIdent.create "&dummy" in
       let convert e =
-        let f = (ss_inv_of_expr (EcIdent.create "&dummy") e).inv in
+        let f = (ss_inv_of_expr dummy_mem e).inv in
 
         if Mid.is_empty alpha then f else