--- a/agda/finiteSet.agda	Fri Nov 22 17:35:12 2019 +0900
+++ b/agda/finiteSet.agda	Fri Nov 22 19:30:10 2019 +0900
@@ -338,8 +338,32 @@
           ∎  where
             open ≡-Reasoning
 
-L2F-iso : { Q : Set } → {n : ℕ } → (fin : FiniteSet Q {n}) → (f : Q → Bool ) → (q : Q ) → (List2Func a<sa fin (F2L a<sa fin (λ q _ → f q) )) q ≡ f q
-L2F-iso {Q} {m} fin f q = l2f m a<sa where
-    l2f :  (n : ℕ ) → (n<m : n < suc m )→  (List2Func n<m fin (F2L n<m  fin (λ q _ → f q))) q ≡ f q
-    l2f zero (s≤s z≤n) = ?
-    l2f (suc n) n<m = {!!}
+
+L2F : {Q : Set } {n m : ℕ } → n < suc m → (fin : FiniteSet Q {m} )  → Vec Bool n → (q :  Q ) → toℕ (FiniteSet.F←Q fin q ) < n  → Bool
+L2F n<m fin x q q<n = List2Func n<m fin x q 
+
+L2F-iso : { Q : Set } → {n : ℕ } → (fin : FiniteSet Q {n}) → (f : Q → Bool ) → (q : Q ) → (L2F a<sa fin (F2L a<sa fin (λ q _ → f q) )) q (toℕ<n _) ≡ f q
+L2F-iso {Q} {m} fin f q = l2f m a<sa (toℕ<n _) where
+    lemma11 : {n : ℕ } → (n<m : n < m )  → ¬ ( FiniteSet.F←Q fin q ≡ fromℕ≤ n<m ) → toℕ (FiniteSet.F←Q fin q) ≤ n → toℕ (FiniteSet.F←Q fin q) < n
+    lemma11 {n} n<m ¬q=n q≤n = lemma13 n<m (contra-position (lemma12 n<m _) ¬q=n ) q≤n where
+       lemma13 : {n nq : ℕ } → (n<m : n < m )  → ¬ ( nq ≡ n ) → nq  ≤ n → nq < n
+       lemma13 {0} {0} (s≤s z≤n) nt z≤n = ⊥-elim ( nt refl )
+       lemma13 {suc _} {0} (s≤s (s≤s n<m)) nt z≤n = s≤s z≤n
+       lemma13 {suc n} {suc nq} n<m nt (s≤s nq≤n) = s≤s (lemma13 {n} {nq} (Data.Nat.Properties.<-trans a<sa n<m ) (λ eq → nt ( cong ( λ k → suc k ) eq )) nq≤n)
+       lemma3 : {a b : ℕ } → (lt : a < b ) → fromℕ≤ (s≤s lt) ≡ suc (fromℕ≤ lt)
+       lemma3 (s≤s lt) = refl
+       lemma12 : {n m : ℕ } → (n<m : n < m ) → (f : Fin m )  → toℕ f ≡ n → f ≡ fromℕ≤ n<m 
+       lemma12 {zero} {suc m} (s≤s z≤n) zero refl = refl
+       lemma12 {suc n} {suc m} (s≤s n<m) (suc f) refl = subst ( λ k → suc f ≡ k ) (sym (lemma3 n<m) ) ( cong ( λ k → suc k ) ( lemma12 {n} {m} n<m f refl  ) )
+    l2f :  (n : ℕ ) → (n<m : n < suc m ) → (q<n : toℕ (FiniteSet.F←Q fin q ) < n )  →  (L2F n<m fin (F2L n<m  fin (λ q _ → f q))) q q<n ≡ f q
+    l2f zero (s≤s z≤n) ()
+    l2f (suc n) (s≤s n<m) (s≤s n<q) with FiniteSet.F←Q fin q ≟ fromℕ≤ n<m
+    l2f (suc n) (s≤s n<m) (s≤s n<q) | yes p with f q
+    l2f (suc n) (s≤s n<m) (s≤s n<q) | yes p | true = refl -- f (FiniteSet.Q←F fin (fromℕ≤ n<m)) !=< true
+    l2f (suc n) (s≤s n<m) (s≤s n<q) | yes p | false = {!!}
+    --         {!!}
+    --      ≡⟨ {!!}  ⟩
+    --        f q
+    --      ∎  where
+    --        open ≡-Reasoning
+    l2f (suc n) (s≤s n<m) (s≤s n<q) | no ¬p = l2f n (Data.Nat.Properties.<-trans n<m a<sa) (lemma11 n<m ¬p n<q)