diff --git a/Fixedpoint.agda b/Fixedpoint.agda
index 388fcaf..1ce26cf 100644
--- a/Fixedpoint.agda
+++ b/Fixedpoint.agda
@@ -13,6 +13,7 @@ module Fixedpoint {a} {A : Set a}
 
 open import Data.Nat.Properties using (+-suc; +-comm)
 open import Data.Product using (_×_; Σ; _,_; proj₁; proj₂)
+open import Data.Empty using (⊥-elim)
 open import Relation.Binary.PropositionalEquality using (_≡_; sym)
 open import Relation.Nullary using (Dec; ¬_; yes; no)
 
@@ -30,7 +31,7 @@ private
     ...   | yes a≈⊥ᴬ = ≼-cong a≈⊥ᴬ ≈-refl (≼-refl a)
     ...   | no a̷≈⊥ᴬ with ≈-dec ⊥ᴬ (a ⊓ ⊥ᴬ)
     ...         | yes ⊥ᴬ≈a⊓⊥ᴬ = (a , ≈-trans (⊔-comm ⊥ᴬ a) (≈-trans (≈-⊔-cong (≈-refl {a}) ⊥ᴬ≈a⊓⊥ᴬ) (absorb-⊔-⊓ a ⊥ᴬ)))
-    ...         | no ⊥ᴬ̷≈a⊓⊥ᴬ = absurd (ChainA.Bounded-suc-n (proj₂ fixedHeight) (ChainA.step x≺⊥ᴬ ≈-refl (proj₂ (proj₁ fixedHeight))))
+    ...         | no ⊥ᴬ̷≈a⊓⊥ᴬ = ⊥-elim (ChainA.Bounded-suc-n (proj₂ fixedHeight) (ChainA.step x≺⊥ᴬ ≈-refl (proj₂ (proj₁ fixedHeight))))
                     where
                         ⊥ᴬ⊓a̷≈⊥ᴬ : ¬ (⊥ᴬ ⊓ a) ≈ ⊥ᴬ
                         ⊥ᴬ⊓a̷≈⊥ᴬ = λ ⊥ᴬ⊓a≈⊥ᴬ → ⊥ᴬ̷≈a⊓⊥ᴬ (≈-trans (≈-sym ⊥ᴬ⊓a≈⊥ᴬ) (⊓-comm _ _))
@@ -44,7 +45,7 @@ private
     -- out, we have exceeded h steps, which shouldn't be possible.
 
     doStep : ∀ (g hᶜ : ℕ) (a₁ a₂ : A) (c : ChainA.Chain a₁ a₂ hᶜ) (g+hᶜ≡h : g + hᶜ ≡ suc h) (a₂≼fa₂ : a₂ ≼ f a₂) → Σ A (λ a → a ≈ f a)
-    doStep 0 hᶜ a₁ a₂ c g+hᶜ≡sh a₂≼fa₂ rewrite g+hᶜ≡sh = absurd (ChainA.Bounded-suc-n (proj₂ fixedHeight) c)
+    doStep 0 hᶜ a₁ a₂ c g+hᶜ≡sh a₂≼fa₂ rewrite g+hᶜ≡sh = ⊥-elim (ChainA.Bounded-suc-n (proj₂ fixedHeight) c)
     doStep (suc g') hᶜ a₁ a₂ c g+hᶜ≡sh a₂≼fa₂ rewrite sym (+-suc g' hᶜ)
         with ≈-dec a₂ (f a₂)
     ...   | yes a₂≈fa₂ = (a₂ , a₂≈fa₂)
@@ -70,7 +71,7 @@ private
                      (c : ChainA.Chain a₁ a₂ hᶜ) (g+hᶜ≡h : g + hᶜ ≡ suc h)
                      (a₂≼fa₂ : a₂ ≼ f a₂) →
                      proj₁ (doStep g hᶜ a₁ a₂ c g+hᶜ≡h a₂≼fa₂) ≼ a
-    stepPreservesLess 0 _ _ _ _ _ _ c g+hᶜ≡sh _ rewrite g+hᶜ≡sh = absurd (ChainA.Bounded-suc-n (proj₂ fixedHeight) c)
+    stepPreservesLess 0 _ _ _ _ _ _ c g+hᶜ≡sh _ rewrite g+hᶜ≡sh = ⊥-elim (ChainA.Bounded-suc-n (proj₂ fixedHeight) c)
     stepPreservesLess (suc g') hᶜ a₁ a₂ a a≈fa a₂≼a c g+hᶜ≡sh a₂≼fa₂ rewrite sym (+-suc g' hᶜ)
         with ≈-dec a₂ (f a₂)
     ...   | yes _ = a₂≼a