fixes #2466 (#2478)

Co-authored-by: MatthewDaggitt <[email protected]>

Author: jamesmckinna

CHANGELOG.md

@@ -125,6 +125,8 @@ Additions to existing modules
 
 * In `Data.List.Membership.Setoid.Properties`:
   ```agda
+  ∉⇒All[≉]       : x ∉ xs → All (x ≉_) xs
+  All[≉]⇒∉       : All (x ≉_) xs → x ∉ xs
   Any-∈-swap     : Any (_∈ ys) xs → Any (_∈ xs) ys
   All-∉-swap     : All (_∉ ys) xs → All (_∉ xs) ys
   ∈-map∘filter⁻  : y ∈₂ map f (filter P? xs) → ∃[ x ] x ∈₁ xs × y ≈₂ f x × P x

src/Data/List/Membership/Setoid/Properties.agda

@@ -75,6 +75,14 @@ module _ (S : Setoid c ℓ) where
   ∉-resp-≋ : ∀ {x} → (x ∉_) Respects _≋_
   ∉-resp-≋ xs≋ys v∉xs v∈ys = v∉xs (∈-resp-≋ (≋-sym xs≋ys) v∈ys)
 
+  -- x ∉_ is equivalent to All (x ≉_)
+
+  ∉⇒All[≉] : ∀ {x xs} → x ∉ xs → All (x ≉_) xs
+  ∉⇒All[≉] = All.¬Any⇒All¬ _
+
+  All[≉]⇒∉ : ∀ {x xs} → All (x ≉_) xs → x ∉ xs
+  All[≉]⇒∉ = All.All¬⇒¬Any
+
   -- index is injective in its first argument.
 
   index-injective : ∀ {x₁ x₂ xs} (x₁∈xs : x₁ ∈ xs) (x₂∈xs : x₂ ∈ xs) →
@@ -93,7 +101,7 @@ module _ (S : Setoid c ℓ) where
 
   private
     ∉×∈⇒≉ : ∀ {x y xs} → All (y ≉_) xs → x ∈ xs → x ≉ y
-    ∉×∈⇒≉ = All.lookupWith λ y≉z x≈z x≈y → y≉z (trans (sym x≈y) x≈z)
+    ∉×∈⇒≉ ≉s x∈xs x≈y = All[≉]⇒∉ S ≉s (∈-resp-≈ S x≈y x∈xs)
 
   unique⇒irrelevant : Binary.Irrelevant _≈_ → ∀ {xs} → Unique xs → Unary.Irrelevant (_∈ xs)
   unique⇒irrelevant ≈-irr _        (here p)  (here q)  =