diff --git a/src/ThesisWork/Pi3S2/SuccStr.agda b/src/ThesisWork/Pi3S2/SuccStr.agda
index ba3ee18..8aab348 100644
--- a/src/ThesisWork/Pi3S2/SuccStr.agda
+++ b/src/ThesisWork/Pi3S2/SuccStr.agda
@@ -27,8 +27,23 @@ module _ where
   open import Data.Fin
   open import Data.Product
 
+  inc-k-inv : {k : ℕ} → (ℕ × Fin k) → (ℕ × Fin k)
+  inc-k-inv {k} (n , zero) = (suc n) , opposite zero
+  inc-k-inv {k} (n , suc k1) = n , inject₁ k1
+
+  inc : {k : ℕ} → (ℕ × Fin k) → (ℕ × Fin k)
+  inc {k} (n , k1) =
+    let result = inc-k-inv (n , opposite k1) in
+    (fst result) , opposite (snd result)
+
+  _ : inc {k = 3} (5 , fromℕ 2) ≡ (6 , zero)
+  _ = refl
+
+  -- _ : inc {k = 3} (5 , inject₁ (fromℕ 1)) ≡ (6 , zero)
+  -- _ = {!  refl !}
+
+  _ : inc {k = 5} (5 , fromℕ 4) ≡ (6 , zero)
+  _ = refl
+
   ℕ-k-SuccStr : (k : ℕ) → (ℕ × Fin k) → ℕ → (ℕ × Fin k)
-  ℕ-k-SuccStr k = SuccStr (ℕ × Fin k) inc where
-    inc : (ℕ × Fin k) → (ℕ × Fin k)
-    inc (n , k) with suc k
-    inc (n , k) | x = {!   !}
\ No newline at end of file
+  ℕ-k-SuccStr k = SuccStr (ℕ × Fin k) inc
\ No newline at end of file