Change ⊥-elim to contradiction in src/Codata/Guarded/Stream/Relation/Unary/Any.agda (#2652)

Author: jmougeot

src/Codata/Guarded/Stream/Relation/Unary/Any.agda

@@ -9,10 +9,9 @@
 module Codata.Guarded.Stream.Relation.Unary.Any where
 
 open import Codata.Guarded.Stream as Stream using (Stream)
-open import Data.Empty using (⊥-elim)
 open import Data.Nat.Base hiding (_⊔_)
 open import Level hiding (zero; suc)
-open import Relation.Nullary.Negation.Core using (¬_)
+open import Relation.Nullary.Negation.Core using (¬_; contradiction)
 open import Relation.Unary using (Pred; _⊆_)
 
 private
@@ -28,10 +27,10 @@ data Any {A : Set a} (P : Pred A p) : Stream A → Set (a ⊔ p) where
 
 head : ¬ Any P (Stream.tail xs) → Any P xs → P (Stream.head xs)
 head ¬t (here h) = h
-head ¬t (there t) = ⊥-elim (¬t t)
+head ¬t (there t) = contradiction t ¬t
 
 tail : ¬ P (Stream.head xs) → Any P xs → Any P (Stream.tail xs)
-tail ¬h (here h) = ⊥-elim (¬h h)
+tail ¬h (here h) = contradiction h ¬h
 tail ¬h (there t) = t
 
 map : P ⊆ Q → Any P ⊆ Any Q