[Refractor] contradiction over ⊥-elim in as def (#2660)

* [Refractor] contradiction over ⊥-elim in as def

* [Refractor] contradiction over ⊥-elim in as def

* Update src/Relation/Binary/Construct/StrictToNonStrict.agda

Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com>

* Narrowing

---------

Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com>

Author: jmougeot

src/Relation/Binary/Construct/StrictToNonStrict.agda

@@ -28,7 +28,8 @@ open import Relation.Binary.Structures
 open import Relation.Binary.Definitions
   using (Transitive; Symmetric; Irreflexive; Antisymmetric; Trichotomous; Decidable
         ; Trans; Total; _Respects₂_; _Respectsʳ_; _Respectsˡ_; tri<; tri≈; tri>)
-open import Relation.Nullary.Decidable using (_⊎-dec_; yes; no)
+open import Relation.Nullary.Decidable.Core using (_⊎-dec_; yes; no)
+open import Relation.Nullary.Negation.Core using (contradiction)
 
 ------------------------------------------------------------------------
 -- Conversion
@@ -59,7 +60,7 @@ antisym eq trans irrefl = as
   as (inj₂ x≈y) _          = x≈y
   as (inj₁ _)   (inj₂ y≈x) = Eq.sym y≈x
   as (inj₁ x<y) (inj₁ y<x) =
-    ⊥-elim (trans∧irr⇒asym {_≈_ = _≈_} Eq.refl trans irrefl x<y y<x)
+    contradiction y<x (trans∧irr⇒asym {_≈_ = _≈_} Eq.refl trans irrefl x<y)
 
 trans : IsEquivalence _≈_ → _<_ Respects₂ _≈_ → Transitive _<_ →
         Transitive _≤_

src/Tactic/RingSolver/NonReflective.agda

@@ -21,7 +21,6 @@ open import Algebra.Morphism
 open import Function.Base using (id; _⟨_⟩_)
 open import Data.Bool.Base using (Bool; true; false; T; if_then_else_)
 open import Data.Maybe.Base
-open import Data.Empty using (⊥-elim)
 open import Data.Nat.Base using (ℕ)
 open import Data.Product.Base using (_×_; proj₁; proj₂; _,_)
 open import Data.Vec.Base using (Vec)