--- a/agda/finiteSet.agda	Fri Nov 08 14:42:28 2019 +0900
+++ b/agda/finiteSet.agda	Fri Nov 08 16:26:40 2019 +0900
@@ -8,6 +8,8 @@
 open import Relation.Binary.Core
 open import Relation.Binary.PropositionalEquality
 open import logic
+open import nat
+open import Data.Nat.Properties  hiding ( _≟_ )
 
 record FiniteSet ( Q : Set ) { n : ℕ }
         : Set  where
@@ -52,23 +54,24 @@
      fin<n {_} {zero} = s≤s z≤n
      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 (lt0 n) (toℕ (F←Q q)) fin<n where
-         q=q : (i : Fin n) → i ≡ F←Q q → p (Q←F i) ≡ true 
-         q=q = {!!}
-         found1 : (m : ℕ ) → (m<n : m Data.Nat.≤ n ) (qn : ℕ ) → qn < m → exists1 m m<n p ≡ true
-         found1 zero _ _ () 
-         found1 (suc m) m<n qn qn<m with Data.Nat._≟_ m qn
-         found1 (suc m) m<n qn qn<m | yes refl = {!!}
-         found1 (suc m) m<n zero qn<m | no ¬p = {!!}
-         found1 (suc m) m<n (suc qn) qn<m | no ¬p = begin
-                  p (Q←F (fromℕ≤ m<n)) \/ exists1 m (lt2 m<n) p
-              ≡⟨ {!!}  ⟩
-                  false \/ exists1 m (lt2 m<n) p
-              ≡⟨ bool-or-1 refl  ⟩
-                  exists1 m (lt2 m<n) p
-              ≡⟨ found1 m (lt2 m<n) qn {!!} ⟩
-                  true
+     found {p} {q} pt = found1 n (fin<n {n} {F←Q q}) (lt0 n) lemma1 where
+         lemma : {i m : ℕ} (i≤n : (suc i) Data.Nat.≤ m ) → (m<n : m Data.Nat.≤ n ) → (suc i) Data.Nat.≤ n
+         lemma = Data.Nat.Properties.≤-trans
+         lemma1 : Q←F (fromℕ≤ (lemma fin<n (lt0 n))) ≡ q
+         lemma1 = {!!}
+         found1 : (m : ℕ ) {i : ℕ } → (i≤m : (suc i) Data.Nat.≤ m ) → (m<n : m Data.Nat.≤ n ) → Q←F (fromℕ≤ {i} {n} (lemma i≤m m<n)) ≡ q → exists1 m m<n p ≡ true
+         found1 (suc m) {i} lt m<n iq with Data.Nat._≟_ m i
+         found1 (suc m) {i} lt m<n iq | yes refl = begin
+                 p (Q←F (fromℕ≤ m<n )) \/ exists1 m (lt2 m<n ) p
+              ≡⟨ cong (λ k → (p k \/ exists1 m (lt2 m<n ) p )) (subst (λ k → k ≡ q) ? iq ) ⟩
+                 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
+              ≡⟨⟩
+                 true 
               ∎  where open ≡-Reasoning
+         found1 (suc m) {i} lt m<n iq | no ¬p = {!!}
+             
 
 fless : {n : ℕ} → (f : Fin n ) → toℕ f < n
 fless zero = s≤s z≤n