--- a/FLutil.agda	Thu Nov 26 14:09:54 2020 +0900
+++ b/FLutil.agda	Fri Nov 27 08:55:59 2020 +0900
@@ -71,7 +71,6 @@
 FL0 {zero} = f0
 FL0 {suc n} = zero :: FL0
 
-
 fmax : { n : ℕ } →  FL n
 fmax {zero} = f0
 fmax {suc n} = fromℕ< a<sa :: fmax {n}
@@ -161,6 +160,45 @@
 -- fr5 : List (List ℕ)
 -- fr5 = map plist (map FL→perm  (Data.List.reverse (flist (fmax {4}) )))
 
+FL1 : List ℕ → List ℕ
+FL1 [] = []
+FL1 (x ∷ y) = suc x ∷ FL1 y
+
+FL→plist : {n : ℕ} → FL n → List ℕ
+FL→plist {0} f0 = []
+FL→plist {suc n} (zero :: y) = zero ∷ FL1 (FL→plist y) 
+FL→plist {suc n} (suc x :: y) with FL→plist y
+... | [] = zero ∷ []
+... | x1 ∷ t = suc x1 ∷ FL2 x t where
+  FL2 : {n : ℕ} → Fin n → List ℕ → List ℕ
+  FL2 zero y = zero ∷ FL1 y
+  FL2 (suc i) [] = zero ∷ []
+  FL2 (suc i) (x ∷ y) = suc x ∷ FL2 i y
+
+tt0 = (# 2) :: (# 1) :: (# 0) :: zero :: f0
+tt1 = FL→plist tt0
+-- tt2 = plist ( FL→perm tt0 )
+
+open _∧_
+
+find-zero : {n i : ℕ} → List ℕ → i < n  → Fin n ∧ List ℕ
+find-zero  [] i<n = record { proj1 = fromℕ< i<n  ; proj2 = [] }
+find-zero x (s≤s z≤n) = record { proj1 = fromℕ< (s≤s z≤n)  ; proj2 = x }
+find-zero (zero ∷ y) (s≤s (s≤s i<n)) = record { proj1 = fromℕ< (s≤s (s≤s i<n)) ; proj2 = y }
+find-zero (suc x ∷ y) (s≤s (s≤s i<n)) with find-zero y (s≤s i<n) 
+... | record { proj1 = i ; proj2 = y1 } = record { proj1 = suc i ; proj2 = suc x ∷ y1 }
+
+plist→FL : {n : ℕ} → List ℕ → FL n
+plist→FL {zero} [] = f0
+plist→FL {suc n} [] = zero :: plist→FL {n} []
+plist→FL {zero} x = f0
+plist→FL {suc n} x with find-zero x a<sa
+... | record { proj1 = i ; proj2 = y } = i :: plist→FL y
+
+tt2 = 2 ∷ 1 ∷ 0 ∷ 3 ∷ []
+tt3 : FL 4
+tt3 = plist→FL tt2
+-- tt4 = proj1 (find-zero {5} {4} tt2 a<sa) , proj2 (find-zero {5} {4} tt2 a<sa)
 
 open import Relation.Binary as B hiding (Decidable; _⇔_)
 open import Data.Sum.Base as Sum --  inj₁
@@ -266,8 +304,13 @@
 nextAny (here x₁) = there (here x₁)
 nextAny (there any) = there (there any)
 
-postulate
-   AnyFList : {n : ℕ }  → (x : FL n ) →  Any (x ≡_ ) (∀Flist fmax)
+
+AnyFList : {n : ℕ }  → (x : FL n ) →  Any (x ≡_ ) (∀Flist fmax)
+AnyFList {zero} f0 = here refl
+AnyFList {suc zero} (x :: f0) = ?
+AnyFList {suc (suc n)} (x :: y) = AnyFList1 (suc n) a<sa (∀Flist fmax) (∀Flist fmax) fin<n (AnyFList y) where
+   AnyFList1 :  (i : ℕ) → (i<n : i < suc (suc n) ) → (L L1 : FList (suc n) ) → toℕ x < suc i → Any (y ≡_ ) L1 → Any ((x :: y) ≡_ ) (Flist i i<n L L1)
+   AnyFList1 = {!!} 
 
 -- FLinsert membership