--- a/agda/finiteSet.agda	Fri Nov 08 16:26:40 2019 +0900
+++ b/agda/finiteSet.agda	Fri Nov 08 19:52:26 2019 +0900
@@ -11,6 +11,9 @@
 open import nat
 open import Data.Nat.Properties  hiding ( _≟_ )
 
+open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
+
+
 record FiniteSet ( Q : Set ) { n : ℕ }
         : Set  where
      field
@@ -53,24 +56,44 @@
      fin<n : {n : ℕ} {f : Fin n} → toℕ f < n
      fin<n {_} {zero} = s≤s z≤n
      fin<n {suc n} {suc f} = s≤s (fin<n {n} {f})
+     <s : {m : ℕ} → m Data.Nat.≤ suc m
+     <s {zero} = z≤n
+     <s {suc m} = s≤s <s
+     lemma0 : {n : ℕ } {i j : ℕ } → i ≡ j → ( i<n : (suc i) Data.Nat.≤ n ) → ( j<n : (suc j) Data.Nat.≤ n ) → i<n ≅ j<n
+     lemma0 {_} {0} {0} refl (s≤s z≤n) (s≤s z≤n) = HE.refl
+     lemma0 {suc n} {suc i} {suc i} refl (s≤s (s≤s x)) (s≤s (s≤s y))  = HE.cong ( λ k → s≤s k) (lemma0 {n} {i} {i} refl (s≤s x)  (s≤s y))
+     lemma : {n : ℕ } {i j : ℕ } → i ≡ j → { i<n : (suc i) Data.Nat.≤ n } → { j<n : (suc j) Data.Nat.≤ n } → fromℕ≤ i<n ≅ fromℕ≤ j<n
+     lemma refl {x} {y} = HE.cong ( λ k → fromℕ≤ k ) ( lemma0 refl x y )
+     lemma1 : {i m : ℕ } (i≤m : (suc i) Data.Nat.≤ m ) (m<n : m Data.Nat.≤ n ) → i < n
+     lemma1 {i} {m} i≤m m<n =  Data.Nat.Properties.≤-trans i≤m m<n 
      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) 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
+     found {p} {q} pt = found1 n (toℕ (F←Q q)) (fin<n {n} {F←Q q}) (lt0 n) {!!} where
+         lemma2 : F←Q q ≅ fromℕ≤ (lemma1 (fin<n {n} {F←Q q}) (lt0 n))
+         lemma2 = {!!}
+         lemma3 : {m i : ℕ} → ( m<n : m Data.Nat.≤ n ) → (i≤m : i Data.Nat.≤ suc m )
+             → (iq :  F←Q q ≅ fromℕ≤ {i} {n} {!!} ) → Q←F (fromℕ≤ {!!}) ≡ q
+         lemma3 = {!!}
+         found1 : (m : ℕ ) (i : ℕ) (i≤m : (suc i) Data.Nat.≤ m ) (m<n : m Data.Nat.≤ n ) ( iq : F←Q q ≡ fromℕ≤ {i} (lemma1 i≤m m<n) ) →  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 ) ⟩
+              ≡⟨ cong (λ k → (p k \/ exists1 m (lt2 m<n ) p )) (
+                 begin
+                    Q←F (fromℕ≤ m<n) 
+                 ≡⟨ lemma HE.refl ⟩
+                    Q←F (fromℕ≤ {i} (lemma1 lt m<n))
+                 ≡⟨ cong ( λ k → Q←F k ) (sym iq)  ⟩
+                    Q←F (F←Q 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
               ≡⟨⟩
                  true 
               ∎  where open ≡-Reasoning
-         found1 (suc m) {i} lt m<n iq | no ¬p = {!!}
+         found1 (suc m) i lt m<n iq | no ¬p = {!!}
              
 
 fless : {n : ℕ} → (f : Fin n ) → toℕ f < n