# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1606698802 -32400
# Node ID 6c81c3d535d152a73897560e01d6bca9edae2782
# Parent  c93a60686dcec76868f6cc3614991ea53056ae54
...

diff -r c93a60686dce -r 6c81c3d535d1 FLutil.agda
--- a/FLutil.agda	Mon Nov 30 08:07:55 2020 +0900
+++ b/FLutil.agda	Mon Nov 30 10:13:22 2020 +0900
@@ -322,10 +322,16 @@
    AnyFList1 :  (i x : ℕ) → (i<n : i < suc (suc n) ) → (L L1 : FList (suc n) ) → (x<n : x < suc (suc n) ) → x < suc i → Any (y ≡_ ) L
         → Any (((fromℕ< x<n) :: y) ≡_ ) (Flist i i<n L L1)
    AnyFList1 zero x i<n [] L1 (s≤s x<i) _ ()
-   AnyFList1 zero zero i<n (cons a L xr) L1 x<n (s≤s z≤n) (here refl) = x∈FLins (zero :: a) (Flist 0 i<n L L1)
-   AnyFList1 zero zero i<n (cons a L xr) L1 x<n (s≤s z≤n) (there wh) with AnyFList1 zero zero i<n L L1 x<n (s≤s z≤n) wh
-   ... | t = {!!}
-   AnyFList1 (suc i) x i<n L L1 x<n x<i wh = {!!}
+   AnyFList1 zero zero i<n (cons y L xr) L1 x<n (s≤s z≤n) (here refl) = x∈FLins (zero :: y) (Flist 0 i<n L L1)
+   AnyFList1 zero zero i<n (cons a L xr) L1 x<n (s≤s z≤n) (there wh) = insAny _ (AnyFList1 zero zero i<n L L1 x<n (s≤s z≤n) wh)
+   AnyFList1 (suc i) x (s≤s i<n) (cons y L x₁) L1 x<n (s≤s x<i) (here refl) with <-fcmp (fromℕ< x<n) (fromℕ< (s≤s i<n))
+   ... | tri< a ¬b ¬c = insAny _ af1 where
+        af1 : Any (_≡_ (fromℕ< x<n :: y)) (Flist (suc i) (s≤s i<n) L L1)
+        af1 = AnyFList1 (suc i) x (s≤s i<n) L L1 x<n (s≤s x<i) {!!}
+   ... | tri≈ ¬a b ¬c = subst (λ k → Any (_≡_ (fromℕ< x<n :: y)) (FLinsert k  (Flist (suc i) (s≤s i<n) L L1) )) (cong (λ k → k :: y) b)
+        (x∈FLins (fromℕ< x<n :: y) (Flist (suc i) (s≤s i<n) L L1))
+   ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> x<i (subst₂ (λ j k → suc (suc k) ≤ j ) (toℕ-fromℕ< _) (toℕ-fromℕ< _) c) )
+   AnyFList1 (suc i) x i<n (cons a L x₁) L1 x<n (s≤s x<i) (there wh) = {!!}
 
 -- FLinsert membership