diff --git a/src/Fancy/Prod.v b/src/Fancy/Prod.v
index 45df4844b3..f421bab684 100644
--- a/src/Fancy/Prod.v
+++ b/src/Fancy/Prod.v
@@ -114,7 +114,7 @@ Ltac step_rhs :=
   match goal with
   | H: ?x = spec ?i ?args _
     |- context [spec ?i ?args ?cc] =>
-    replace (spec i args cc) with x by idtac
+    replace (spec i args cc) with x by first [assumption | symmetry;assumption]
   end;
   match goal with
   | H : ?y = (?x mod ?m)%Z |- context [(?x mod ?m)%Z] =>
@@ -397,4 +397,4 @@ Ltac push_value_unused :=
          | _ => apply not_in_cons; split;
                 [ try assumption; symmetry; assumption | ]
          | _ => apply in_nil
-         end.
\ No newline at end of file
+         end.