diff --git a/FiniteSets/disjunction.v b/FiniteSets/disjunction.v
index d198ace..fe8c1dd 100644
--- a/FiniteSets/disjunction.v
+++ b/FiniteSets/disjunction.v
@@ -84,7 +84,7 @@ Open Scope logic_scope.
 Section hPropLattice.
   Context `{Univalence}.
 
-  Instance lor_commutative : Commutative lor.
+  Global Instance lor_commutative : Commutative lor.
   Proof.
     unfold Commutative.
     intros.
@@ -182,11 +182,4 @@ Section hPropLattice.
       absorption_max_min := _
   }.
   
-End hPropLattice.
-
-Hint Resolve
-     commutative_min commutative_max associative_min associative_max
-     idempotent_min idempotent_max
-     neutralL_min neutralR_min
-     absorption_min_max absorption_max_min
- : lattice_hints.
\ No newline at end of file
+End hPropLattice.
\ No newline at end of file
diff --git a/FiniteSets/fsets/operations.v b/FiniteSets/fsets/operations.v
index 81c6bf0..0da4ff9 100644
--- a/FiniteSets/fsets/operations.v
+++ b/FiniteSets/fsets/operations.v
@@ -17,9 +17,9 @@ hrecursion.
   exact _.
 - apply lor.
 - intros ; symmetry ; apply lor_assoc.
-- intros ; apply lor_comm.
-- intros ; apply lor_nl.
-- intros ; apply lor_nr.
+- apply lor_commutative.
+- apply lor_nl.
+- apply lor_nr.
 - intros ; apply lor_idem.
 Defined.