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

Author: jmougeot

src/Data/List/Fresh/Relation/Unary/All/Properties.agda

@@ -10,12 +10,10 @@ module Data.List.Fresh.Relation.Unary.All.Properties where
 
 open import Data.List.Fresh using (List#; []; cons; _∷#_; _#_)
 open import Data.List.Fresh.Relation.Unary.All using (All; []; _∷_; append)
-open import Data.Empty using (⊥; ⊥-elim)
 open import Data.Nat.Base using (ℕ; zero; suc)
 open import Data.Product.Base using (_,_)
 open import Function.Base using (_∘′_)
 open import Level using (Level; _⊔_; Lift)
-open import Relation.Nullary.Negation.Core using (¬_)
 open import Relation.Unary  as U using (Pred)
 open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong)

src/Data/List/Fresh/Relation/Unary/Any/Properties.agda

@@ -9,7 +9,6 @@
 module Data.List.Fresh.Relation.Unary.Any.Properties where
 
 open import Data.Bool.Base using (true; false)
-open import Data.Empty using (⊥; ⊥-elim)
 open import Data.List.Fresh using (List#; _∷#_; _#_; NonEmpty; cons; length; [])
 open import Data.List.Fresh.Relation.Unary.All using (All; _∷_; append; [])
 open import Data.List.Fresh.Relation.Unary.Any using (Any; here; there; _─_)
@@ -19,12 +18,12 @@ open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂)
 open import Function.Base using (_∘′_)
 open import Level using (Level; _⊔_; Lift)
 open import Relation.Nullary.Reflects using (invert)
-open import Relation.Nullary.Negation.Core using (¬_)
 open import Relation.Nullary.Decidable.Core
 open import Relation.Unary  as U using (Pred)
 open import Relation.Binary.Core using (Rel)
 open import Relation.Nary using (∀[_]; _⇒_; ∁; Decidable)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong)
+open import Relation.Nullary.Negation.Core using (contradiction; ¬_)
 
 private
   variable
@@ -56,15 +55,15 @@ module _ {R : Rel A r} {P : Pred A p} {Q : Pred A q} (P⇒¬Q : ∀[ P ⇒ ∁ Q
 module _ {R : Rel A r} {P : Pred A p} {Q : Pred A q} (P? : Decidable P) where
 
   ¬All⇒Any : {xs : List# A R} → ¬ (All P xs) → Any (∁ P) xs
-  ¬All⇒Any {xs = []}      ¬ps = ⊥-elim (¬ps [])
+  ¬All⇒Any {xs = []}      ¬ps = contradiction [] ¬ps
   ¬All⇒Any {xs = x ∷# xs} ¬ps with P? x
   ... |  true because  [p] = there (¬All⇒Any (¬ps ∘′ (invert [p] ∷_)))
   ... | false because [¬p] = here (invert [¬p])
 
   ¬Any⇒All : {xs : List# A R} → ¬ (Any P xs) → All (∁ P) xs
   ¬Any⇒All {xs = []}      ¬ps = []
   ¬Any⇒All {xs = x ∷# xs} ¬ps with P? x
-  ... |  true because  [p] = ⊥-elim (¬ps (here (invert [p])))
+  ... |  true because  [p] = contradiction (here (invert [p])) ¬ps
   ... | false because [¬p] = invert [¬p] ∷ ¬Any⇒All (¬ps ∘′ there)
 
 ------------------------------------------------------------------------