--- a/automaton-in-agda/src/finiteSetUtil.agda	Tue Jul 18 18:54:46 2023 +0900
+++ b/automaton-in-agda/src/finiteSetUtil.agda	Tue Jul 18 19:21:51 2023 +0900
@@ -700,12 +700,26 @@
     cb00 : (n : ℕ) → n < count-B (finite fa) → CountB n
     cb00 n n<cb = lem09 (finite fa) (count-B (finite fa)) (<-transˡ a<sa n<cb) refl where
 
+        lem06 : (i j : ℕ) → (i<fa : i < finite fa) (j<fa : j < finite fa) 
+            →  Is B A f (Q←F fa (fromℕ< i<fa)) → Is B A f (Q←F fa (fromℕ< j<fa)) → count-B i ≡ count-B j → i ≡ j
+        lem06 i j i<fa j<fa bi bj eq = ? where
+            lem20 : (i j : ℕ) → i < j → (i<fa : i < finite fa) (j<fa : j < finite fa) 
+                →  Is B A f (Q←F fa (fromℕ< i<fa)) → Is B A f (Q←F fa (fromℕ< j<fa)) → count-B j ≡ count-B i → ⊥
+            lem20 zero (suc j) i<j bi bj le = ?
+            lem20 (suc i) zero () bi bj le
+            lem20 (suc i) (suc j) (s≤s i<j) bi bj le = ?
+            lem08 : i ≡ j
+            lem08 with <-cmp i j
+            ... | tri< a ¬b ¬c = ⊥-elim ( lem20 i j a ? ? bi bj (sym eq) )
+            ... | tri≈ ¬a b ¬c = b
+            ... | tri> ¬a ¬b c₁ = ⊥-elim ( lem20 j i c₁ ? ? bj bi eq )
+
         lem09 : (i j : ℕ) →  suc n ≤ j → j ≡ count-B i →  CountB n
         lem09 0 (suc j) (s≤s le) eq with is-B (Q←F fa (fromℕ< {0} 0<fa )) | inspect count-B 0
         ... | no nisb | record { eq = eq1 } = ⊥-elim ( nat-≡< (sym eq) (s≤s z≤n) )
         ... | yes isb | record { eq = eq1 } with ≤-∨ (s≤s le)
         ... | case1 eq2 = record { b = Is.a isb ; cb = 0 ; b=cn = lem10 ; cb=n = trans eq1 (sym (trans eq2 eq))
-                ; cb-inject = λ cb1 iscb1 cb1eq →  ?} where
+                ; cb-inject = ? } where
              lem10 : 0 ≡ toℕ (F←Q fa (f (Is.a isb)))
              lem10 = begin
                 0 ≡⟨ sym ( toℕ-fromℕ< 0<fa ) ⟩