# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1607502835 -32400
# Node ID f45298e34491853bd81eea1175ae4e9e5db933e2
# Parent  c3a67bb7cbc0c27f935820348baa514eb92434d9
anyFL done

diff -r c3a67bb7cbc0 -r f45298e34491 FLComm.agda
--- a/FLComm.agda	Wed Dec 09 17:18:05 2020 +0900
+++ b/FLComm.agda	Wed Dec 09 17:33:55 2020 +0900
@@ -86,15 +86,13 @@
         anyFL6 (cons _ xs _) (here refl) refl = x∈FLins (x :: y)  (allListFL zero xs z)
         anyFL6 (cons _ xs  _) (there any) refl = insAny _ (anyFL6 xs any refl )
     anyFL3 {suc i} (s≤s (s≤s i<n)) (x :: y) x<i z with <-cmp (toℕ x) (suc i)
-    ... | tri< a ¬b ¬c = anyFL1 (s≤s i<n) where
-        anyFL1  : {i : ℕ} → (i<n : i < suc n) →  Any (_≡_ (x :: y)) (allListF (s≤s i<n) z)
-        anyFL10 : {j : ℕ} → (i<n : j < suc n ) → (x<i : toℕ x ≤ suc i) → (L : FList (suc n))  
+    ... | tri< a ¬b ¬c = anyFL1 (s≤s i<n) a where
+        anyFL1  : {i : ℕ} → (i<n : i < suc n) → (x<i : suc (toℕ x) ≤ suc i )  →  Any (_≡_ (x :: y)) (allListF (s≤s i<n) z)
+        anyFL10 : {i : ℕ} → (i<n : i < suc n ) → (x<i : suc (toℕ x) ≤ suc i) → (L : FList (suc n))  
             → Any (_≡_ (x :: y))  (allListFL (suc (fromℕ< i<n)) L (allListF (<-trans i<n a<sa) z) )
-        anyFL10 {j} (s≤s j<n) x<i [] = anyFL3 (<-trans (s≤s j<n) a<sa) (x :: y) (anyFL11 x<i)  z   where
-             anyFL11 : toℕ x ≤ suc i → toℕ x ≤ j 
-             anyFL11 = {!!}
+        anyFL10 {i} (s≤s j<n) (s≤s x<i) [] = anyFL3 (<-trans (s≤s j<n) a<sa) (x :: y) x<i z  --  where suc (toℕ x) ≤ suc i → toℕ x ≤ i
         anyFL10 {i} i<n x<i (cons _ xs _)  = insAny _ (anyFL10 {i} i<n x<i xs )
-        anyFL1 (s≤s i<n) = anyFL10 (s≤s i<n ) x<i (allFL (anyFL0 n)) 
+        anyFL1 {i} (s≤s i<n) x<i = anyFL10 (s≤s i<n ) x<i (allFL (anyFL0 n)) 
     ... | tri≈ ¬a b ¬c = anyFL7 (allFL (anyFL0 n)) (anyP (anyFL0 n) y) where
         anyFL9 : toℕ x ≡ suc i → x ≡ suc (fromℕ< (s≤s i<n))
         anyFL9 x=si = toℕ-injective ( begin