diff --git a/FrapWithoutSets.v b/FrapWithoutSets.v
index ae8e051..01e29b3 100644
--- a/FrapWithoutSets.v
+++ b/FrapWithoutSets.v
@@ -234,6 +234,10 @@ Qed.
 Ltac sets0 := Sets.sets ltac:(simpl in *; intuition (subst; auto; try equality; try linear_arithmetic)).
 
 Ltac sets := propositional;
+  try match goal with
+      | [ |- @eq (?T -> Prop) _ _ ] =>
+        change (T -> Prop) with (set T)
+      end;
   try match goal with
       | [ |- @eq (set _) _ _ ] =>
         let x := fresh "x" in