diff --git a/FiniteSets/fsets/operations.v b/FiniteSets/fsets/operations.v
index 6484e78..034fe0d 100644
--- a/FiniteSets/fsets/operations.v
+++ b/FiniteSets/fsets/operations.v
@@ -45,7 +45,6 @@ Section operations.
   Proof.
     simple refine (FSet_rec _ _ _ true (fun _ => false) andb _ _ _ _ _)
     ; try eauto with bool_lattice_hints typeclass_instances.
-    intros ; symmetry ; eauto with lattice_hints typeclass_instances.
   Defined.
 
   Definition single_product {A B : Type} (a : A) : FSet B -> FSet (A * B).
diff --git a/FiniteSets/lattice.v b/FiniteSets/lattice.v
index fe55e25..97358eb 100644
--- a/FiniteSets/lattice.v
+++ b/FiniteSets/lattice.v
@@ -37,6 +37,7 @@ Arguments JoinSemiLattice _ {_} {_}.
 
 Create HintDb joinsemilattice_hints.
 Hint Resolve associativity : joinsemilattice_hints.
+Hint Resolve (associativity _ _ _)^ : joinsemilattice_hints.
 Hint Resolve commutative : joinsemilattice_hints.
 Hint Resolve idempotency : joinsemilattice_hints.
 Hint Resolve neutralityL : joinsemilattice_hints.
@@ -65,6 +66,7 @@ Arguments Lattice _ {_} {_} {_}.
 
 Create HintDb lattice_hints.
 Hint Resolve associativity : lattice_hints.
+Hint Resolve (associativity _ _ _)^ : lattice_hints.
 Hint Resolve commutative : lattice_hints.
 Hint Resolve absorb : lattice_hints.
 Hint Resolve idempotency : lattice_hints.
@@ -189,6 +191,7 @@ End sub_lattice.
 
 Create HintDb bool_lattice_hints.
 Hint Resolve associativity : bool_lattice_hints.
+Hint Resolve (associativity _ _ _)^ : bool_lattice_hints.
 Hint Resolve commutative : bool_lattice_hints.
 Hint Resolve absorb : bool_lattice_hints.
 Hint Resolve idempotency : bool_lattice_hints.