# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1573212215 -32400
# Node ID 7c38ed740961d455d72a310e416e646f4d95bef3
# Parent  184752a8f0edc634e5e6cf23e3da56dd57216e65
...

diff -r 184752a8f0ed -r 7c38ed740961 agda/finiteSet.agda
--- a/agda/finiteSet.agda	Fri Nov 08 20:18:10 2019 +0900
+++ b/agda/finiteSet.agda	Fri Nov 08 20:23:35 2019 +0900
@@ -58,19 +58,19 @@
      fin<n {suc n} {suc f} = s≤s (fin<n {n} {f})
      found : { p : Q → Bool } → {q : Q } → p q ≡ true → exists p ≡ true
      found {p} {q} pt = found1 n  (fin<n {n} {F←Q q}) (lt0 n) where
-         iq : {m : ℕ} (lt : suc m Data.Nat.≤ n ) → toℕ (F←Q q) ≡ m → Q←F (fromℕ≤ lt) ≡ q
-         iq {m} lt refl = begin
-                 Q←F (fromℕ≤ lt) 
-              ≡⟨ {!!} ⟩
-                 Q←F (F←Q q)
-              ≡⟨ finiso→ q ⟩
-                 q 
-              ∎  where open ≡-Reasoning
          found1 : (m : ℕ ) {i : ℕ} (i≤m : (suc i) Data.Nat.≤ m ) (m<n : m Data.Nat.≤ n ) →  exists1 m m<n p ≡ true
-         found1 (suc m)  lt m<n with Data.Nat._≟_ m (toℕ (F←Q q))
-         found1 (suc m)  lt m<n | yes refl = begin
+         found1 0 ()
+         found1 (suc m)  lt m<n with fromℕ≤ m<n ≟ F←Q q
+         found1 (suc m)  lt m<n | yes eq = begin
                  p (Q←F (fromℕ≤ m<n )) \/ exists1 m (lt2 m<n ) p
-              ≡⟨ cong (λ k → (p k \/ exists1 m (lt2 m<n ) p )) (iq m<n refl ) ⟩
+              ≡⟨ cong (λ k → (p k \/ exists1 m (lt2 m<n ) p )) (
+                 begin
+                    Q←F (fromℕ≤ m<n)
+                 ≡⟨ cong ( λ k → Q←F k ) eq ⟩
+                    Q←F (F←Q q)
+                 ≡⟨ finiso→  q ⟩
+                    q
+                 ∎ ) ⟩
                  p q \/ exists1 m (lt2 m<n ) p
               ≡⟨ cong (λ k → ( k \/ exists1 m (lt2 m<n ) p )) pt ⟩
                   true \/ exists1 m (lt2 m<n ) p