# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1600129545 -32400
# Node ID 88585eeb917cd82194c6bfd9d69feba2bd027e83
# Parent  61bfb2c5e03ddacc48ca9f3b8ce1b113a714a07e
...

diff -r 61bfb2c5e03d -r 88585eeb917c FLutil.agda
--- a/FLutil.agda	Tue Sep 15 09:00:23 2020 +0900
+++ b/FLutil.agda	Tue Sep 15 09:25:45 2020 +0900
@@ -221,13 +221,19 @@
 x∈FLins {suc n} x (cons a [] x₁)              | tri> ¬a ¬b a<x = there ( here refl )
 x∈FLins {suc n} x (cons a (cons a₁ xs x₂) x₁) | tri> ¬a ¬b a<x = there ( x∈FLins x (cons a₁ xs x₂) )
 
+open import fin
+
 x∈∀Flist : {n : ℕ } → (x : FL n ) → Any (x ≡_ ) (∀Flist fmax)
 x∈∀Flist {n} x  = AFlist1 n x where
+    AFList0 : (n : ℕ ) →  Any (_≡_ (fromℕ< a<sa :: fmax)) (Flist1 n a<sa (∀Flist fmax) (∀Flist fmax))
+    AFList0 = {!!}
+    AFList2 : (n : ℕ )  (x : FL (suc n)) → (x1 : Fin (suc n)) (y : FL n) → x f< ( x1 :: y)  → Any (_≡_ x) (Flist1 n a<sa (∀Flist y) (∀Flist y))
+    AFList2 = {!!}
     AFlist1 : (n : ℕ ) → (x : FL n)  → Any (_≡_ x) (∀Flist fmax)
     AFlist1 zero f0 = here refl
     AFlist1 (suc n) x with FLcmp x fmax 
-    ... | tri< a ¬b ¬c = {!!}
-    ... | tri≈ ¬a refl ¬c = {!!}
+    ... | tri< a ¬b ¬c = AFList2 n x (fromℕ< a<sa) (fmax {n}) (fmax¬ ¬b)
+    ... | tri≈ ¬a refl ¬c = AFList0 n
     ... | tri> ¬a ¬b c = ⊥-elim ( fmax< c )