diff --git a/agda/src/Monad/Instance/Setoids/K.lagda.md b/agda/src/Monad/Instance/Setoids/K.lagda.md
index d2ee949..b511d27 100644
--- a/agda/src/Monad/Instance/Setoids/K.lagda.md
+++ b/agda/src/Monad/Instance/Setoids/K.lagda.md
@@ -323,11 +323,9 @@ To show preservation we need some facts about discretizing setoids:
       cong (disc-dom {X} f) {x} {y} x≡y rewrite x≡y = ≡-refl (Delay∼.₀ A ⊎ₛ ‖ X ‖) 
 
       iter-g-var : ∀ {X : Setoid ℓ ℓ} → (g : X ⟶ (Delay≈.₀ A ⊎ₛ X)) → ∀ {x} → [ A ][ (iter {A} {X} < g >) x ∼ (iter∼ {A} {‖ X ‖} (disc-dom g)) ⟨$⟩ x ]
-      iter-g-var′ : ∀ {X : Setoid ℓ ℓ} → (g : X ⟶ (Delay≈.₀ A ⊎ₛ X)) → ∀ {x} → [ A ][ (iter {A} {X} < g >) x ∼′ (iter∼ {A} {‖ X ‖} (disc-dom g)) ⟨$⟩ x ]
-      force∼ (iter-g-var′ {X} g {x}) = iter-g-var {X} g {x}
       iter-g-var {X} g {x} with g ⟨$⟩ x
       ...                  | inj₁ a = ∼-refl A
-      ...                  | inj₂ a = later∼ (iter-g-var′ {X} g {a})
+      ...                  | inj₂ a = later∼ λ { .force∼ → iter-g-var {X} g {a} }
 ```
 
 Now we show that helper # is iteration preserving: