[Refractor] contradiction over ⊥-elim inData/List/Fresh/Membership/Setoid/Properties

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

@@ -32,6 +32,7 @@ import Relation.Binary.Definitions as Binary using (_Respectsˡ_; Irrelevant)
 import Relation.Binary.PropositionalEquality.Core as ≡
   using (_≡_; cong; sym; subst)
 open import Relation.Nary using (∀[_]; _⇒_)
+open import Relation.Nullary.Negation using (contradiction)
 
 open Setoid S renaming (Carrier to A)
 
@@ -132,7 +133,7 @@ module _ {R : Rel A r} (R⇒≉ : ∀[ R ⇒ _≉_ ]) where
     open ≤-Reasoning
 
     step : ∀ {y} → y ∈ xs → y ∈ (ys ─ x∈ys)
-    step {y} y∈xs = fromInj₂ (λ x≈y → ⊥-elim (x∉xs (≈-subst-∈ (sym x≈y) y∈xs)))
+    step {y} y∈xs = fromInj₂ (λ x≈y → contradiction (≈-subst-∈ (sym x≈y) y∈xs) x∉xs )
                   $ remove-inv x∈ys (inj y∈xs)
 
 
@@ -147,6 +148,6 @@ module _ {R : Rel A r} (R⇒≉ : ∀[ R ⇒ _≉_ ]) (≈-irrelevant : Binary.I
   ∈-irrelevant (there x∈xs₁) (there x∈xs₂) = ≡.cong there (∈-irrelevant x∈xs₁ x∈xs₂)
   -- absurd cases
   ∈-irrelevant {xs = cons x xs pr} (here x≈y)    (there x∈xs₂) =
-    ⊥-elim (distinct x∈xs₂ (fresh⇒∉ R⇒≉ pr) x≈y)
+    contradiction x≈y (distinct x∈xs₂ (fresh⇒∉ R⇒≉ pr))
   ∈-irrelevant {xs = cons x xs pr} (there x∈xs₁) (here x≈y)    =
-    ⊥-elim (distinct x∈xs₁ (fresh⇒∉ R⇒≉ pr) x≈y)
+    contradiction x≈y (distinct x∈xs₁ (fresh⇒∉ R⇒≉ pr))

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

@@ -32,7 +32,7 @@ open import Relation.Binary.Definitions as Binary hiding (Decidable)
 open import Relation.Binary.Bundles using (Setoid)
 open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
 open import Relation.Nullary.Decidable using (does; _because_; yes; no)
-open import Relation.Nullary.Negation using (¬_; contradiction)
+open import Relation.Nullary.Negation.Core using (¬_; contradiction)
 open import Relation.Nullary.Reflects using (invert)
 open import Relation.Unary as Unary using (Decidable; Pred)