--- a/FLutil.agda	Tue Nov 24 08:43:48 2020 +0900
+++ b/FLutil.agda	Tue Nov 24 11:08:07 2020 +0900
@@ -6,7 +6,7 @@
 open import Data.Fin.Properties hiding ( <-trans ; ≤-refl ; ≤-trans ; ≤-irrelevant ; _≟_ ) renaming ( <-cmp to <-fcmp )
 open import Data.Fin.Permutation  -- hiding ([_,_])
 open import Data.Nat -- using (ℕ; suc; zero; s≤s ; z≤n )
-open import Data.Nat.Properties
+open import Data.Nat.Properties as DNP
 open import Relation.Binary.PropositionalEquality hiding ( [_] )
 open import Data.List using (List; []; _∷_ ; length ; _++_ ; tail ) renaming (reverse to rev )
 open import Data.Product
@@ -226,6 +226,10 @@
 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₂) )
 
+nextAny : {n : ℕ} → {x h : FL n } → {L : FList n}  → {hr : fresh (FL n) ⌊ _f<?_ ⌋ h L } → Any (x ≡_ ) L → Any (x ≡_ ) (cons h L hr )
+nextAny (here x₁) = there (here x₁)
+nextAny (there any) = there (there any)
+
 open import fin
 
 record ∀FListP (n : ℕ ) : Set (Level.suc Level.zero) where
@@ -235,17 +239,26 @@
 
 open ∀FListP
 
+-- open import Data.Fin.Properties as FinP
+
 AnyFList : (n : ℕ )  → (x : FL n ) →  Any (x ≡_ ) (∀Flist fmax)
 AnyFList n x = AnyFlist0 fmax x where
-   AnyFlist1 :  {n : ℕ } (i : ℕ) → (i<n : i < suc n ) → (x : Fin (suc n)) → toℕ x < suc i → (y : FL n) → (L L1 : FList n )
-       → Any (y ≡_ ) L  →  Any ((x :: y ) ≡_ ) (Flist1 i i<n L L1 )
-   AnyFlist1 zero i<n zero x<i y (cons y L ar) L1 (here refl) = x∈FLins (zero :: y) (Flist1 zero i<n L L1 )
-   AnyFlist1 zero i<n (suc x) (s≤s ()) y (cons y L ar) L1 (here refl)
-   AnyFlist1 (suc i) i<n x x<i y (cons y L ar) L1 (here refl) = ?
-   AnyFlist1 i i<n x x<i y (cons a L ar) L1 (there any) = {!!}
+   AnyFlist1 :  {n : ℕ } (i : ℕ) → (i<n : i < suc n ) → (x : Fin (suc n)) → (y : FL n) → toℕ x < suc i → (L L1 : FList n )
+       → Any (y ≡_ ) L1 → Any (y ≡_ ) L →  Any ((x :: y ) ≡_ ) (Flist1 i i<n L L1 )
+   AnyFlist1 zero i<n zero y (s≤s x<i) (cons _ L _) L1 any (here refl) = x∈FLins (zero :: y) (Flist1 zero i<n L L1 )
+   AnyFlist1 zero i<n zero y (s≤s x<i) (cons a L ar) L1 any (there any0) = anf0 (AnyFlist1 zero i<n zero y (s≤s x<i) L L1 any any0) where
+        anf0 :  Any ((zero :: y ) ≡_ ) (Flist1 zero i<n L L1) → Any (_≡_ (zero :: y)) (Flist1 zero i<n (cons a L ar) L1)
+        anf0 = {!!}
+   AnyFlist1 (suc i) i<n x y x<i (cons y L ar) L1 any (here refl) with <-fcmp x (fromℕ< i<n)
+   ... | tri≈ ¬a refl ¬c = subst {!!} {!!} (x∈FLins (x :: y) (Flist1 (suc i) i<n L L1 ))
+   ... | tri> ¬a ¬b c = {!!}
+   ... | tri< a ¬b ¬c with AnyFlist1 i {!!} x y {!!} L1 L1 any any 
+   ... | t = {!!}
+   AnyFlist1 (suc i) i<n x y x<i (cons a L ar) L1 any (there any0) with AnyFlist1 (suc i) i<n x y x<i L L1 any any0
+   ... | t = {!!}
    AnyFlist0 : {n : ℕ } → (y x : FL n ) →  Any (x ≡_ ) (∀Flist y)
    AnyFlist0 {zero} f0 f0 = here refl
-   AnyFlist0 {suc n} (_ :: z) (x :: y) = AnyFlist1 n a<sa x fin<n y (∀Flist z) (∀Flist z) (AnyFlist0 z y) where
+   AnyFlist0 {suc n} (_ :: z) (x :: y) = AnyFlist1 n a<sa x y fin<n (∀Flist z) (∀Flist z) (AnyFlist0 z y) (AnyFlist0 z y)
 
 -- tt1 : FList 3
 -- tt1 = ∀FListP.∀list (∀FList 3)