[Refractor] contradiction over ⊥-elim in (agda#2667)

Author: jmougeot

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.Core 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))