diff --git a/prelude/collections.v b/prelude/collections.v
index cf4669c0a7b492625c0d63ad7d5905466c5e9a01..41610062cf8a3c5b3fcd8a3729758e48f7d0c0f3 100644
--- a/prelude/collections.v
+++ b/prelude/collections.v
@@ -265,7 +265,7 @@ Ltac set_unfold :=
 [set_solver] already. We use the [naive_solver] tactic as a substitute.
 This tactic either fails or proves the goal. *)
 Tactic Notation "set_solver" "by" tactic3(tac) :=
-  try done;
+  try (reflexivity || eassumption);
   intros; setoid_subst;
   set_unfold;
   intros; setoid_subst;