diff --git a/src/ecPV.ml b/src/ecPV.ml
index 04fb55032..19c763f24 100644
--- a/src/ecPV.ml
+++ b/src/ecPV.ml
@@ -1139,6 +1139,10 @@ 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.inter fv1 fv2))
     | _, _ -> raise EqObsInError
 
   let add_eqs env e1 e2 eqs =  add_eqs_loc env Mid.empty eqs e1 e2