diff --git a/src/foundation/multisubsets.lagda.md b/src/foundation/multisubsets.lagda.md
index dcf3673b6e..004d510e28 100644
--- a/src/foundation/multisubsets.lagda.md
+++ b/src/foundation/multisubsets.lagda.md
@@ -12,6 +12,7 @@ open import elementary-number-theory.natural-numbers
 open import foundation.dependent-pair-types
 open import foundation.images
 open import foundation.negated-equality
+open import foundation.function-types
 open import foundation.universe-levels
 
 open import foundation-core.fibers-of-maps
@@ -56,7 +57,7 @@ module _
   support-locally-finite-multisubset :
     (U : Set l1) → locally-finite-multisubset U → UU l1
   support-locally-finite-multisubset U μ =
-    Σ (type-Set U) (λ x → μ x ≠ zero-ℕ)
+    Σ (type-Set U) (λ {≠ → precomp μ UU (_≠ 0) ≠})
 
   is-finite-locally-finite-multisubset :
     (U : Set l1) → locally-finite-multisubset U → UU l1