contradiction against ⊥-elim

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

@@ -8,7 +8,6 @@
 
 module Data.List.Relation.Unary.Any where
 
-open import Data.Empty
 open import Data.Fin.Base using (Fin; zero; suc)
 open import Data.List.Base as List using (List; []; [_]; _∷_; removeAt)
 open import Data.Product.Base as Product using (∃; _,_)
@@ -46,7 +45,7 @@ head ¬pxs (here px)   = px
 head ¬pxs (there pxs) = contradiction pxs ¬pxs
 
 tail : ¬ P x → Any P (x ∷ xs) → Any P xs
-tail ¬px (here  px)  = ⊥-elim (¬px px)
+tail ¬px (here  px)  = contradiction px ¬px
 tail ¬px (there pxs) = pxs
 
 map : P ⊆ Q → Any P ⊆ Any Q