diff --git a/agda/src/Monad/Instance/Setoids/K.lagda.md b/agda/src/Monad/Instance/Setoids/K.lagda.md
index 2de8e86..ed03469 100644
--- a/agda/src/Monad/Instance/Setoids/K.lagda.md
+++ b/agda/src/Monad/Instance/Setoids/K.lagda.md
@@ -182,7 +182,7 @@ module Monad.Instance.Setoids.K {ℓ : Level} where
 
 
   delay-lift : ∀ {A : Setoid ℓ ℓ} {B : Elgot-Algebra} → A ⟶ ⟦ B ⟧ → Elgot-Algebra-Morphism (delay-algebras A) B
-  delay-lift {A} {B} f = record { h = delay-lift' ; preserves = λ {X} {g} {x} → ≡-trans ⟦ B ⟧ (preserves' {X} {g} {x}) (#-resp-≈ B (≡-refl (⟦ B ⟧ ⊎ₛ X))) }
+  delay-lift {A} {B} f = record { h = delay-lift' ; preserves = λ {X} {g} {x} → preserves' {X} {g} {x} }
     where
     open Elgot-Algebra B using (_#)
     -- (f + id) ∘ out
@@ -296,7 +296,7 @@ module Monad.Instance.Setoids.K {ℓ : Level} where
           where
             eq' : ∀ {n} → [ ⟦ B ⟧ ⊎ₛ Delayₛ∼ A ][ [ inj₁ , inj₂ ∘′ μ ∘′ liftF ι ] (helper₁' (now (x , n))) ≡ (helper₁ ∘′ μ {A} ∘′ liftF ι) (now (y , n)) ]
             eq' {zero}  = inj₁ (cong f x∼y)
-            eq' {suc n} = inj₂ (∼-trans A (cong (μₛ∼ A) (∼-sym (Delayₛ∼ A) (lift-comp∼ {f = outer} {g = ιₛ'} {ι (x , n)} (∼-refl A)))) (∼-trans A identityˡ∼ (cong ιₛ' (x∼y , ≣-refl)))) -- (identityˡ∼ (cong ιₛ' (x∼y , ≣-refl))))
+            eq' {suc n} = inj₂ (∼-trans A (cong (μₛ∼ A) (∼-sym (Delayₛ∼ A) (lift-comp∼ {f = outer} {g = ιₛ'} {ι (x , n)} (∼-refl A)))) (∼-trans A identityˡ∼ (cong ιₛ' (x∼y , ≣-refl))))
         eq (later∼ x∼y) = inj₂ (cong (μₛ∼ A) (cong (liftFₛ∼ ιₛ') (force∼ x∼y)))
 
         eq₂ : [ ⟦ B ⟧ ][ helper' # ⟨$⟩ z ≡ helper # ⟨$⟩ μ {A} (liftF (ι {A}) z)]
@@ -329,7 +329,19 @@ module Monad.Instance.Setoids.K {ℓ : Level} where
     preserves' {X} {g} {x} = ≡-trans ⟦ B ⟧ step₁ step₂
       where
       step₁ : [ ⟦ B ⟧ ][ (delay-lift' ∘ (iterₛ {A} {X} g)) ⟨$⟩ x ≡ ([ inj₁ₛ ∘ (helper #) , inj₂ₛ ]ₛ ∘ (disc-dom g)) # ⟨$⟩ x ]
-      step₁ = {!   !}
+      step₁ = ≡-trans ⟦ B ⟧ (≡-trans ⟦ B ⟧ (helper#∼-cong (iter-g-var g)) (sub-step₁ (disc-dom g) {inj₂ x})) (≡-sym ⟦ B ⟧ (#-Compositionality B {f = helper} {h = disc-dom g}))
+        where
+          sub-step₁ : (g : ‖ X ‖ ⟶ ((Delayₛ∼ A) ⊎ₛ ‖ X ‖)) → ∀ {x} → [ ⟦ B ⟧ ][ ((helper #) ∘ [ idₛ (Delayₛ∼ A) , iterₛ∼ g ]ₛ) ⟨$⟩ x
+            ≡ ([ [ inj₁ₛ , inj₂ₛ ∘ inj₁ₛ ]ₛ ∘ helper , inj₂ₛ ∘ inj₂ₛ ]ₛ ∘ [ inj₁ₛ , g ]ₛ) # ⟨$⟩ x ]
+          sub-step₁ g {u} = ≡-sym ⟦ B ⟧ (#-Uniformity B {h = [ idₛ (Delayₛ∼ A) , iterₛ∼ g ]ₛ} (λ {y} → last-step {y}))
+            where
+            last-step : ∀ {x} → [ ⟦ B ⟧ ⊎ₛ (Delayₛ∼ A) ][ [ inj₁ₛ , inj₂ₛ ∘ [ idₛ (Delayₛ∼ A) , iterₛ∼ g ]ₛ ]ₛ ∘ [ [ inj₁ₛ , inj₂ₛ ∘ inj₁ₛ ]ₛ ∘ helper , inj₂ₛ ∘ inj₂ₛ ]ₛ ∘ [ inj₁ₛ , g ]ₛ ⟨$⟩ x ≡ (helper ∘ [ idₛ (Delayₛ∼ A) , iterₛ∼ g ]ₛ) ⟨$⟩ x ]
+            last-step {inj₁ (now a)} = ≡-refl (⟦ B ⟧ ⊎ₛ (Delayₛ∼ A))
+            last-step {inj₁ (later a)} = ≡-refl (⟦ B ⟧ ⊎ₛ (Delayₛ∼ A))
+            last-step {inj₂ a} with g ⟨$⟩ a in eqb
+            ...                | inj₁ (now b) = ≡-refl (⟦ B ⟧ ⊎ₛ (Delayₛ∼ A))
+            ...                | inj₁ (later b) = ≡-refl (⟦ B ⟧ ⊎ₛ (Delayₛ∼ A))
+            ...                | inj₂ b = ≡-refl (⟦ B ⟧ ⊎ₛ (Delayₛ∼ A))
       step₂ : [ ⟦ B ⟧ ][ ([ inj₁ₛ ∘ (helper #) , inj₂ₛ ]ₛ ∘ (disc-dom g)) # ⟨$⟩ x ≡ ([ inj₁ₛ ∘ delay-lift' , inj₂ₛ ]ₛ ∘ g) # ⟨$⟩ x ]
       step₂ = #-Uniformity B {h = ‖‖-quote} sub-step₂
         where
@@ -337,8 +349,6 @@ module Monad.Instance.Setoids.K {ℓ : Level} where
           sub-step₂ {x} with g ⟨$⟩ x
           ... | inj₁ y = ≡-refl (⟦ B ⟧ ⊎ₛ X)
           ... | inj₂ y = ≡-refl (⟦ B ⟧ ⊎ₛ X)
-      comp-step : [ ⟦ B ⟧ ][ ([ inj₁ₛ ∘ (helper #) , inj₂ₛ ]ₛ ∘ disc-dom g) # ⟨$⟩ x ≡ ((([ ([ inj₁ₛ , (inj₂ₛ ∘ inj₁ₛ) ]ₛ ∘ helper) , (inj₂ₛ ∘ inj₂ₛ) ]ₛ ∘ [ inj₁ₛ , (disc-dom g) ]ₛ) #) ∘ inj₂ₛ) ⟨$⟩ x ]
-      comp-step = #-Compositionality B {f = helper} {h = disc-dom g}
 
   <<_>> = Elgot-Algebra-Morphism.h