diff --git a/algebra/upred_big_op.v b/algebra/upred_big_op.v
index ba5c046913556bd47be861012a52bd807b43175f..85e2b334696d2fa2a0af9d1c6bee29394ef9840f 100644
--- a/algebra/upred_big_op.v
+++ b/algebra/upred_big_op.v
@@ -123,13 +123,10 @@ Section gmap.
   Lemma big_sepM_proper Φ Ψ m :
     (∀ k x, m !! k = Some x → Φ k x ⊣⊢ Ψ k x) →
     ([★ map] k ↦ x ∈ m, Φ k x) ⊣⊢ ([★ map] k ↦ x ∈ m, Ψ k x).
-  Proof. (*
-    (* FIXME: Coq bug since 8.5pl1. Without the @ in [@lookup_weaken] it gives
-    File "./algebra/upred_big_op.v", line 114, characters 4-131:
-    Anomaly: Uncaught exception Univ.AlreadyDeclared. Please report. *)
-    intros [??] ?; apply (anti_symm (⊢)); apply big_sepM_mono;
-      eauto using equiv_entails, equiv_entails_sym, @lookup_weaken.
-  Qed. *) Admitted.
+  Proof.
+    intros ?; apply (anti_symm (⊢)); apply big_sepM_mono;
+      eauto using equiv_entails, equiv_entails_sym, lookup_weaken.
+  Qed.
 
   Global Instance big_sepM_ne m n :
     Proper (pointwise_relation _ (pointwise_relation _ (dist n)) ==> (dist n))