diff --git a/agda/src/Monad/Instance/Setoids/K'.lagda.md b/agda/src/Monad/Instance/Setoids/K'.lagda.md
index 3319e7e..33ce030 100644
--- a/agda/src/Monad/Instance/Setoids/K'.lagda.md
+++ b/agda/src/Monad/Instance/Setoids/K'.lagda.md
@@ -230,15 +230,30 @@ module Monad.Instance.Setoids.K' {ℓ : Level} where
 
         -- Should follow by compositionality + fixpoint
         eq₁ :  [ ⟦ B ⟧ ][ (B Elgot-Algebra.#) helper' ⟨$⟩ z ≡ (B Elgot-Algebra.#) helper ⟨$⟩ liftF proj₁ z ]
-        eq₁ = {!!}
+        eq₁ = {!  !}
+
+
+        -- eq : ∀ {x y} → [ A ×ₛ ℕ-setoid ][ x ∼ y ] → [ ⟦ B ⟧ ⊎ₛ Delayₛ' A ][ [ inj₁ , inj₂ ∘′ μ ∘′ (liftF ι) ] (helper₁' x) ≡ (helper₁ ∘′ μ ∘′ (liftF ι)) y ]
+        -- eq {now (x , zero)} {now (y , zero)} (now∼ (x≡y , _)) = cong (inj₁ₛ {_} {_} {_} {_} {⟦ B ⟧} {Delayₛ' A}) (cong f x≡y)
+        -- eq {now (x , suc n)} {now (y , suc m)} (now∼ (x≡y , n≡m)) with helper₁' (now (x , n)) in eqr
+        -- ...                                                       | inj₁ r = {! eq {now (x , n)} {now (y , m)}  !} -- problem: recursive call to eq does not pass termination checker
+        --   where
+        --     help : [ ⟦ B ⟧ ⊎ₛ Delayₛ' A ][ [ inj₁ , inj₂ ∘′ μ ∘′ (liftF ι) ] (helper₁' (now (x , n))) ≡ inj₁ r ]
+        --     help = cong [ inj₁ₛ , (inj₂ₛ ∘ μₛ∼ A ∘ liftFₛ∼ ιₛ') ]ₛ (≡→≡ eqr)
+        -- ...                                                       | inj₂ r = {!   !}
+        -- eq {.(later _)} {.(later _)} (later∼ x≡y) = cong (inj₂ₛ {_} {_} {_} {_} {⟦ B ⟧} {Delayₛ' A}) (cong (μₛ∼ A) (cong (liftFₛ∼ ιₛ') (force∼ x≡y)))
 
         eq : ∀ {x y} → [ A ×ₛ ℕ-setoid ][ x ∼ y ] → [ ⟦ B ⟧ ⊎ₛ Delayₛ' A ][ [ inj₁ , inj₂ ∘′ μ ∘′ (liftF ι) ] (helper₁' x) ≡ (helper₁ ∘′ μ ∘′ (liftF ι)) y ]
-        eq {now (x , zero)} {now (y , zero)} (now∼ (x≡y , _)) = cong (inj₁ₛ {_} {_} {_} {_} {⟦ B ⟧} {Delayₛ' A}) (cong f x≡y)
-        -- eq {now (x , suc n)} {now (y , suc m)} (now∼ (x≡y , n≡m)) with helper₁' (now (x , n)) 
-        -- ...                                                       | inj₁ r = {!   !} -- <- contradiction!
-        -- ...                                                       | inj₂ r = {!   !}
-        eq {now (x , suc n)} {now (y , suc m)} (now∼ (x≡y , n≡m)) = {!   !}
-        -- TODO induction, by a recursive call to eq, we will get info about helper₁' (now (x , n))
+        eq {now (x , n)} {now (y , m)} (now∼ p∼q) = eq' {n} {m} {x} {y} (now∼ p∼q)
+          where
+            eq' : ∀ {n m x y} → [ A ×ₛ ℕ-setoid ][ now (x , n) ∼ now (y , m) ] → [ ⟦ B ⟧ ⊎ₛ Delayₛ' A ][ [ inj₁ , inj₂ ∘′ μ ∘′ (liftF ι) ] (helper₁' (now (x , n))) ≡ (helper₁ ∘′ μ ∘′ (liftF ι)) (now (y , m)) ]
+            eq' {zero} {zero} {x} {y} (now∼ (x≡y , _)) = cong (inj₁ₛ {_} {_} {_} {_} {⟦ B ⟧} {Delayₛ' A}) (cong f x≡y)
+            eq' {suc n} {suc m} {x} {y} (now∼ (x≡y , sn≡sm)) with helper₁' (now (x , n)) in eqr 
+            ...                     | inj₁ r = ≡-trans (⟦ B ⟧ ⊎ₛ Delayₛ' A) (≡-sym (⟦ B ⟧ ⊎ₛ Delayₛ' A) help) (≡-trans (⟦ B ⟧ ⊎ₛ Delayₛ' A) (eq' {n} {m} {x} {y} (now∼ (x≡y , suc-inj sn≡sm))) {! -should this be provable?-  !})
+              where
+                help : [ ⟦ B ⟧ ⊎ₛ Delayₛ' A ][ [ inj₁ , inj₂ ∘′ μ ∘′ (liftF ι) ] (helper₁' (now (x , n))) ≡ inj₁ r ]
+                help = cong [ inj₁ₛ , (inj₂ₛ ∘ μₛ∼ A ∘ liftFₛ∼ ιₛ') ]ₛ (≡→≡ eqr)
+            ...                     | inj₂ r = {!   !}
         eq {.(later _)} {.(later _)} (later∼ x≡y) = cong (inj₂ₛ {_} {_} {_} {_} {⟦ B ⟧} {Delayₛ' A}) (cong (μₛ∼ A) (cong (liftFₛ∼ ιₛ') (force∼ x≡y)))
 
         -- Should follow by uniformity