[Refractor] contradiction over ⊥-elim in commutes-with-∪ def (#2663)

Co-authored-by: jamesmckinna <[email protected]>

Author: jmougeot

src/Data/Nat/InfinitelyOften.agda

@@ -8,17 +8,18 @@
 
 module Data.Nat.InfinitelyOften where
 
-open import Effect.Monad using (RawMonad)
-open import Level using (Level; 0ℓ)
 open import Data.Nat.Base using (ℕ; _≤_; _⊔_; _+_; suc; zero; s≤s)
 open import Data.Nat.Properties
 open import Data.Product.Base as Prod hiding (map)
 open import Data.Sum.Base using (inj₁; inj₂; _⊎_)
+open import Effect.Monad using (RawMonad)
 open import Function.Base using (_∘_; id)
+open import Level using (Level; 0ℓ)
 open import Relation.Binary.PropositionalEquality.Core using (_≢_)
 open import Relation.Nullary.Negation using (¬¬-Monad; call/cc)
 open import Relation.Nullary.Negation.Core using (¬_; contradiction)
 open import Relation.Unary using (Pred; _∪_; _⊆_)
+open import Relation.Nullary.Negation.Core using (contradiction)
 
 open RawMonad (¬¬-Monad {a = 0ℓ})