diff --git a/src/ecReduction.ml b/src/ecReduction.ml
index e10b1dd741..f63d0c49ce 100644
--- a/src/ecReduction.ml
+++ b/src/ecReduction.ml
@@ -1878,6 +1878,7 @@ module User = struct
         let rec doit conds f =
           match sform_of_form (simp f) with
           | SFimp (f1, f2) -> doit (f1 :: conds) f2
+          | SFiff (f1, f2)
           | SFeq  (f1, f2) -> (f1, f2, List.rev conds)
           | _ when ty_equal tbool (EcEnv.ty_hnorm f.f_ty env) ->
             (f, f_true, List.rev conds)