diff --git a/src/Monad/Instance/K/StrongPreElgot.lagda.md b/src/Monad/Instance/K/StrongPreElgot.lagda.md
index 9a3ccfb..21ff349 100644
--- a/src/Monad/Instance/K/StrongPreElgot.lagda.md
+++ b/src/Monad/Instance/K/StrongPreElgot.lagda.md
@@ -166,35 +166,34 @@ isInitialStrongPreElgot = record { ! = !′ ; !-unique = !-unique′ }
               η' X                                                 ∎
         α-strength : ∀ {X Y : Obj} → η' (X × Y) ∘ strengthenK.η (X , Y) ≈ strengthen.η (X , Y) ∘ (idC ⁂ η' Y)
         α-strength {X} {Y} = begin 
-          η' (X × Y) ∘ strengthenK.η (X , Y) ≈⟨ IsStableFreeUniformIterationAlgebra.♯-unique (stable Y) (T.η.η (X × Y)) (η' (X × Y) ∘ strengthenK.η (X , Y)) (sym pres₁) pres₃ ⟩ 
+          η' (X × Y) ∘ strengthenK.η (X , Y)                                                                                ≈⟨ IsStableFreeUniformIterationAlgebra.♯-unique (stable Y) (T.η.η (X × Y)) (η' (X × Y) ∘ strengthenK.η (X , Y)) (sym pres₁) pres₃ ⟩ 
           IsStableFreeUniformIterationAlgebra.[ (stable Y) , Functor.₀ elgot-to-uniformF (T-Alg (X × Y)) ]♯ (T.η.η (X × Y)) ≈⟨ sym (IsStableFreeUniformIterationAlgebra.♯-unique (stable Y) (T.η.η (X × Y)) (strengthen.η (X , Y) ∘ (idC ⁂ η' Y)) (sym pres₂) pres₄) ⟩ 
-          strengthen.η (X , Y) ∘ (idC ⁂ η' Y) ∎
+          strengthen.η (X , Y) ∘ (idC ⁂ η' Y)                                                                               ∎
           where
             pres₁ : (η' (X × Y) ∘ strengthenK.η (X , Y)) ∘ (idC ⁂ ηK.η Y) ≈ T.η.η (X × Y)
             pres₁ = begin 
               (η' (X × Y) ∘ strengthenK.η (X , Y)) ∘ (idC ⁂ ηK.η Y) ≈⟨ pullʳ (τ-η (X , Y)) ⟩ 
-              η' (X × Y) ∘ ηK.η (X × Y) ≈⟨ α-η ⟩ 
-              T.η.η (X × Y) ∎
+              η' (X × Y) ∘ ηK.η (X × Y)                             ≈⟨ α-η ⟩ 
+              T.η.η (X × Y)                                         ∎
             pres₂ : (strengthen.η (X , Y) ∘ (idC ⁂ η' Y)) ∘ (idC ⁂ ηK.η Y) ≈ T.η.η (X × Y)
             pres₂ = begin 
               (strengthen.η (X , Y) ∘ (idC ⁂ η' Y)) ∘ (idC ⁂ ηK.η Y) ≈⟨ pullʳ (⁂∘⁂ ○ ⁂-cong₂ identity² α-η) ⟩ 
-              strengthen.η (X , Y) ∘ (idC ⁂ T.η.η Y) ≈⟨ SM.η-comm ⟩ 
-              T.η.η (X × Y) ∎
+              strengthen.η (X , Y) ∘ (idC ⁂ T.η.η Y)                 ≈⟨ SM.η-comm ⟩ 
+              T.η.η (X × Y)                                          ∎
             pres₃ : ∀ {Z : Obj} (h : Z ⇒ K.₀ Y + Z) → (η' (X × Y) ∘ strengthenK.η (X , Y)) ∘ (idC ⁂ h #K) ≈ ((η' (X × Y) ∘ strengthenK.η (X , Y) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #T
             pres₃ {Z} h = begin 
-              (η' (X × Y) ∘ strengthenK.η (X , Y)) ∘ (idC ⁂ h #K) ≈⟨ pullʳ (τ-comm h) ⟩ 
-              η' (X × Y) ∘ ((τ (X , Y) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #K ≈⟨ η'-preserves ((τ (X , Y) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) ⟩ 
+              (η' (X × Y) ∘ strengthenK.η (X , Y)) ∘ (idC ⁂ h #K)                                   ≈⟨ pullʳ (τ-comm h) ⟩ 
+              η' (X × Y) ∘ ((τ (X , Y) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #K                      ≈⟨ η'-preserves ((τ (X , Y) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) ⟩ 
               ((η' (X × Y) +₁ idC) ∘ (strengthenK.η (X , Y) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #T ≈⟨ #-resp-≈ (StrongPreElgotMonad.elgotalgebras A) (pullˡ (+₁∘+₁ ○ +₁-cong₂ refl identity²)) ⟩ 
-              ((η' (X × Y) ∘ strengthenK.η (X , Y) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #T ∎
+              ((η' (X × Y) ∘ strengthenK.η (X , Y) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #T          ∎
             pres₄ : ∀ {Z : Obj} (h : Z ⇒ K.₀ Y + Z) → (strengthen.η (X , Y) ∘ (idC ⁂ η' Y)) ∘ (idC ⁂ h #K) ≈ ((strengthen.η (X , Y) ∘ (idC ⁂ η' Y) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #T
             pres₄ {Z} h = begin 
-              (strengthen.η (X , Y) ∘ (idC ⁂ η' Y)) ∘ (idC ⁂ h #K) ≈⟨ pullʳ (⁂∘⁂ ○ ⁂-cong₂ identity² (η'-preserves h)) ⟩ 
-              strengthen.η (X , Y) ∘ (idC ⁂ ((η' Y +₁ idC) ∘ h) #T) ≈⟨ StrongPreElgotMonad.strengthen-preserves A ((η' Y +₁ idC) ∘ h) ⟩ 
-              ((strengthen.η (X , Y) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ (η' Y +₁ idC) ∘ h)) #T ≈⟨ sym (#-resp-≈ (StrongPreElgotMonad.elgotalgebras A) (refl⟩∘⟨ (pullʳ (⁂∘⁂ ○ ⁂-cong₂ identity² refl)))) ⟩ 
+              (strengthen.η (X , Y) ∘ (idC ⁂ η' Y)) ∘ (idC ⁂ h #K)                                       ≈⟨ pullʳ (⁂∘⁂ ○ ⁂-cong₂ identity² (η'-preserves h)) ⟩ 
+              strengthen.η (X , Y) ∘ (idC ⁂ ((η' Y +₁ idC) ∘ h) #T)                                      ≈⟨ StrongPreElgotMonad.strengthen-preserves A ((η' Y +₁ idC) ∘ h) ⟩ 
+              ((strengthen.η (X , Y) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ (η' Y +₁ idC) ∘ h)) #T             ≈⟨ sym (#-resp-≈ (StrongPreElgotMonad.elgotalgebras A) (refl⟩∘⟨ (pullʳ (⁂∘⁂ ○ ⁂-cong₂ identity² refl)))) ⟩ 
               (((strengthen.η (X , Y) +₁ idC) ∘ (distributeˡ⁻¹ ∘ (idC ⁂ (η' Y +₁ idC))) ∘ (idC ⁂ h)) #T) ≈⟨ sym (#-resp-≈ (StrongPreElgotMonad.elgotalgebras A) (refl⟩∘⟨ (pullˡ ((+₁-cong₂ refl (sym (⟨⟩-unique id-comm id-comm))) ⟩∘⟨refl ○ distribute₁ idC (η' Y) idC)))) ⟩ 
-              -- ((strengthen.η (X , Y) +₁ idC) ∘ ((idC ⁂ η' Y) +₁ (idC ⁂ idC)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #T ≈⟨ {!   !} ⟩ 
-              ((strengthen.η (X , Y) +₁ idC) ∘ ((idC ⁂ η' Y) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #T ≈⟨ #-resp-≈ (StrongPreElgotMonad.elgotalgebras A) (pullˡ (+₁∘+₁ ○ +₁-cong₂ refl identity²)) ⟩ 
-              ((strengthen.η (X , Y) ∘ (idC ⁂ η' Y) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #T ∎
+              ((strengthen.η (X , Y) +₁ idC) ∘ ((idC ⁂ η' Y) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #T     ≈⟨ #-resp-≈ (StrongPreElgotMonad.elgotalgebras A) (pullˡ (+₁∘+₁ ○ +₁-cong₂ refl identity²)) ⟩ 
+              ((strengthen.η (X , Y) ∘ (idC ⁂ η' Y) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #T              ∎
     !-unique′ : ∀ {A : StrongPreElgotMonad} (f : StrongPreElgotMonad-Morphism strongPreElgot A) → StrongPreElgotMonad-Morphism.α (!′ {A = A}) ≃ StrongPreElgotMonad-Morphism.α f
     !-unique′ {A} f {X} = sym (FreeObject.*-uniq
                                 (freeElgot X)