diff --git a/src/Monad/Instance/Delay/Quotienting.lagda.md b/src/Monad/Instance/Delay/Quotienting.lagda.md
index e194936..ff4fb81 100644
--- a/src/Monad/Instance/Delay/Quotienting.lagda.md
+++ b/src/Monad/Instance/Delay/Quotienting.lagda.md
@@ -203,7 +203,7 @@ We will now show that the following conditions are equivalent:
       cond-4 = {!   !}
 
       1⇒2 : cond-1 → cond-2
-      1⇒2 c-1 X = s-alg-on , {!   !}
+      1⇒2 c-1 X = s-alg-on , (begin ρ ∘ μ.η X ≈⟨ D-universal ⟩ Search-Algebra-on.α s-alg-on ∘ D₁ ρ ∎)
         where
           open Coequalizer (coeqs X) renaming (universal to coeq-universal)
           open IsCoequalizer (c-1 X) using () renaming (equality to D-equality; coequalize to D-coequalize; universal to D-universal; unique to D-unique)