Stop relying on replace by automatic assumption-based solving (#1657

)

Before coq/coq#17964 `replace foo with bar by tac` actually means
`replace foo with bar by first [assumption | symmetry; assumption | tac]`.

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.
+         end.