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..cb11a76ef 100644
--- a/src/ecReduction.ml
+++ b/src/ecReduction.ml
@@ -1864,26 +1864,28 @@ let hs_inv_alpha_eq hyps (inv1 : hs_inv) (inv2 : hs_inv) =
 module EqTest = struct
   include EqTest_base
 
-  include EqMod_base(struct
-    let for_expr env ~norm:_ alpha e1 e2 =
-      let convert e =
-        let f = (ss_inv_of_expr (EcIdent.create "&dummy") e).inv in
+  let for_expr env ~norm:_ alpha e1 e2 =
+    let convert e =
+      let f = (ss_inv_of_expr (EcIdent.create "&dummy") e).inv in
+
+      if Mid.is_empty alpha then f else
 
-        if Mid.is_empty alpha then f else
+      let subst =
+        Mid.fold
+          (fun x (y, ty) subst ->
+            Fsubst.f_bind_local subst x (f_local y ty))
+        alpha Fsubst.f_subst_id
 
-        let subst =
-          Mid.fold
-            (fun x (y, ty) subst ->
-              Fsubst.f_bind_local subst x (f_local y ty))
-          alpha Fsubst.f_subst_id
+      in Fsubst.f_subst subst f in
 
-        in Fsubst.f_subst subst f in
+    let f1 = convert e1 in
+    let f2 = convert e2 in
 
-      let f1 = convert e1 in
-      let f2 = convert e2 in
+    is_conv (LDecl.init env []) f1 f2
 
-      is_conv (LDecl.init env []) f1 f2
-   end)
+  include EqMod_base(struct
+    let for_expr = for_expr
+  end)
 
   let for_pv    = fun env ?(norm = true) -> for_pv    env ~norm
   let for_lv    = fun env ?(norm = true) -> for_lv    env ~norm